只需证
apply h
\.
\.
**注意：**当且仅当命题取反之前应当先满足定理条件
example {c : ℝ} (h : c ≠ 0) : Injective fun x ↦ c * x := by
intro x y h'
apply (mul_right_inj' h).mp h'
apply (mul_lt_mul_right epos).mpr
(a0 : 0 < a) : b * a < c * a ↔ b < c #epos为a0的陈述
代入得
rw[·]
nth_rw 1[·] --代入第一个
rw[\l ·]--反向代入
rw [mul_div_cancel₀]
apply h #h为rw命题成立的条件
先证明
have h : ·
取满足特定条件的变量，引入函数自变量，起的作用
intro: x y \epsilon
#epos :\epsilon > 0
#ele1 :\epsilon \leq 1
#xlt :|x| < \epsilon
**注意：**intro事实上会先按照顺序给题目条件起名，再以任取的方式引入新变量
theorem Subset.trans : r ⊆ s → s ⊆ t → r ⊆ t := by
intro rsubs ssubt x xr
exact ssubt (rsubs xr)
按定义化简（目标）
simp only[def]
#or
dsimp
#or
change def
dsimp only [Monotone] at h
rw[def]也可以展开命题的详细定义
rw[abs]可以展开成逻辑与数学语言
term proof 的表示方法
数学语言：
lean语言(Curry)
example {c : ℝ} (mf : Monotone f) (nnc : 0 ≤ c) : Monotone fun x ↦ c * f x :=
fun a b aleb ↦ mul_le_mul_of_nonneg_left (mf aleb) (nnc)
# fun 引入函数变量 在策略证明中为 intro
#\|-> 后证明过程为数学语言证明的逆过程 在策略证明中为apply的过程，可以混用
通过举例证明存在性命题
use instance
proof of the instance
#or term proof
have h: the proof of an instance:= by ...
\< instance,h\>
使用存在性命题
rcases theorem with \< variable, condition\>
#多个存在
rcases h with ⟨a ,ha⟩
rcases ha with ⟨b,hab⟩
##example
{z : ℝ} (h : ∃ x y, z = x ^ 2 + y ^ 2 ∨ z = x ^ 2 + y ^ 2 + 1) : z ≥ 0 := by
rcases h with ⟨x, y, rfl | rfl⟩ # x y为存在的量 rfl为或命题
{z : ℝ} (h : ∃ x y, z = x ^ 2 + y ^ 2 ) : z ≥ 0 := by
rcases h with ⟨x, y, rfl ⟩
# or
rintro
#or
obtain
#or in C03 S02
cases ...
#example
def FnHasLb (f : ℝ → ℝ) :=
∃ a, FnLb f a
(ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
rcases ubf with ⟨a, ubfa⟩
#变量a 对应存在性命题中‘存在’的量，ubfa为存在性命题中a应满足的条件起名
rcases ubg with ⟨b, ubgb⟩
use a + b
apply fnUb_add ubfa ubgb
#example :
FnHasUb f → FnHasUb g → FnHasUb fun x ↦ f x + g x := by
rintro ⟨a, ubfa⟩ ⟨b, ubgb⟩#按顺序引入
#example : #term proof省略关键字
FnHasUb f → FnHasUb g → FnHasUb fun x ↦ f x + g x :=
fun ⟨a, ubfa⟩ ⟨b, ubgb⟩ ↦ ⟨a + b, fnUb_add ubfa ubgb⟩
#example
(ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
obtain ⟨a, ubfa⟩ := ubf
obtain ⟨b, ubgb⟩ := ubg
exact ⟨a + b, fnUb_add ubfa ubgb⟩
更一般的 rcases实现命题的解包
example {f : ℝ → ℝ} (h : Surjective f) : ∃ x, f x ^ 2 = 4 := by
rcases h 2 with ⟨x, hx⟩ #h 为命题名字，2为任意性参数，也可看做该命题的一个参数,\<·\>为存在性参数，可视为命题的实例化
rcases cs (ε /|c|) ecpos with ⟨N , csN⟩ #ecpos为定理要满足的条件
####
A function `f : α → β` is called surjective if every `b : β` is equal to `f a` for some `a : α`
任意性命题的解包
**xfA** : ∀ (i : I), ∃ x_1 ∈ A i, f x_1 = x
解包:rcases xfA i with ⟨yi,yAi,fyx⟩
清除分母
field_simp [h] #h为分母不为0的命题
否命题的证明：在lean中， 意味着 是错误命题
- 证明思路：
#反证
intro A（引入错误命题）
推导到一个否定的公理上
#example
(h : a < b) : ¬b < a := by
intro h'
have : a < a := lt_trans h h'
apply lt_irrefl a this
#example
(h : ∀ a, ∃ x, f x < a) : ¬FnHasLb f := by
intro fnlb
rcases fnlb with ⟨a,fnlba⟩
rcases h a with ⟨ x,hx⟩
have h1 :f x ≥ a := by apply fnlba x
linarith
#example :
¬FnHasUb fun x ↦ x :=by
intro fnub
rcases fnub with ⟨ a,fnuba⟩
have h: a+1 ≤ a:=by apply fnuba (a+1) ### fnuba中有任意性参数（任取x 有f(x)小于a, 会自动进行函数值的计算；若fnuba还有其他条件，并在该条件中已确定了自变量的选取，则不能重复声明。
linarith
正向命题的反证法
###lt_of_not_ge : ¬a ≥ b → a < b
example (h : Monotone f) (h' : f a < f b) : a < b := by
apply lt_of_not_ge #通过运用否命题，将目标转化为非
intro agtb
have h1 : f a ≥ f b:=by apply h agtb --agtb中已经包含了选取哪个自变量的信息，则不用声明自变量选取
linarith
###更一般的 by_contra
example (h : ¬∀ x, P x) : ∃ x, ¬P x := by
by_contra h' #假设原命题的否命题的正确的
apply h
intro x
show P x
by_contra h''
exact h' ⟨x, h''⟩
定义函数：
let f := fun x : ℝ ↦ (0 : ℝ)
证明False时应该如何运用apply？ - Lean 定理证明是curry 化的，通过右结合的定理链条来最终推导出最后的结论； - apply运用定理后，要能直接证明结论 - 证明False链条：正命题 反命题 False
α : Type u_1
P : α → Prop
Q : Prop
h' : ∀ (x : α), P x
x : α
hx : ¬P x
⊢ False
此时证明过程如下所示
(h : ∃ x, ¬P x) : ¬∀ x, P x := by
intro h'
rcases h with ⟨ x,hx⟩
#目标为False，于是先证明反命题
apply hx
非命题的改写-用于命题叙述前面带有 的情况
push_neg at
改写逆否命题
contrapose! h
若h为条件，将h与目标转化为逆否命题形式
若h为命题，则将其转为逆否命题形式
自动矛盾寻找
contradiction
exfalso #将目前的目标替换成False
自动寻找能直接证明目标的假设
assumption
证明A ∧ B及拆解条件中的交命题
#也可用于证明充分必要性命题
constructor
\. proof of A
\. proof of B
example {x y : ℝ} : x ≤ y ∧ ¬y ≤ x ↔ x ≤ y ∧ x ≠ y :=by
#拆为充分性和必要性； constructor # 目标⊢ x ≤ y ∧ ¬y ≤ x → x ≤ y ∧ x ≠ y
· rintro ⟨h0,h1⟩ #拆分目标中的条件，此时不能用constructor拆分目标中的目标
rcases h with ⟨h₀, h₁⟩，可与存在命题解包混用，按顺序声明即可
rintro ⟨h₀, h₁⟩ h'
have ⟨h₀, h₁⟩ := h
match h with
| ⟨h₀, h₁⟩ =>
apply h.right
或命题处理
# 证明或命题
example (h : y > x ^ 2) : y > 0 ∨ y < -1 := by
left #表示选择左边
linarith [pow_two_nonneg x]
#或者
example (h : y > 0) : y > 0 ∨ y < -1 :=
Or.inl h #l表示选择左边
#运用或条件
rcases h with h1 | h2
\. h1 true
\. h2 true
cases le_or_gt 0 y #0 y 表示要代入条件的具体变量
case inl h =>
rw [abs_of_nonneg h]
intro h; left; exact h
case inr h =>
rw [abs_of_neg h]
intro h; right; exact h
#按照命题是否为真分类
example (P : Prop) : ¬¬P → P := by
intro h
by_cases h' : P
\. p is true
\. p is false
且运算的优先级高于或 自动证明的用法
linarith [le_abs_self x, le_abs_self y]:考虑到后两个命题，可使用linarith
证明函数相等
ext x #将f=g转化为证明它们在任意自变量上函数值相等，x ...表示任取的自变量
# 也可类似地运用于证明两个集合相等：\forall x \in A \in B and \forall x \in B \in A
...
其他零零碎碎的关键词1
congr:将目标中|·|=|·|转化为证明·=·
convert 直接运用定理本来的形式，而不需要与目标相关联，之后目标被拆解为证明原始目标和convert之间的关系
univ ：universe 全集 用mem_univ 改写
wlog h：P不失一般性，假设P是对的
\. 证明为什么可以不是一般性
example
{a : ℝ} (h : 1 < a) : a < a * a := by
convert (mul_lt_mul_right _).2 h ##_表示占位
执行完该步骤后，证明信息为
case h.e'_3
a : ℝ
h : 1 < a
⊢ a = 1 * a
case convert_2
a : ℝ
h : 1 < a
⊢ 0 < a
#set
set A := sbSet f g with A_def
# 把A看作sbSet f g
并创建命题 A_def :A = sbSet f g
并进行替换
assumption:自动检查前面有没有假设与结论完全相同
interval_cases m <;> contradiction
--遍历m所属区间的每一个值
创造多个子情况
rvert: rintro的反面
refine' ⟨p, _, pp⟩--refine与exact相同 用-占位,留给后续补充证明,尖括号表示且
tauto
--自动处理一阶逻辑,处理与或非的关系
s.filter h 表示s中满足h的元素构成的子集集合,用mem_filter化简
记作
let N := max Na Nb
集合证明
#转化为存在，任意性语言
rw [subset_def, inter_def, inter_def]
rw [subset_def] at h
#将元素代入集合 a \in set s={x |x>1}，则将 a 写为条件 a>1
simp only [mem_setOf]
# 交和并的处理
交：x ∈ s ∩ t 按定义视为两个命题：x ∈ s and x ∈ t
并：x ∈ s ∪ t 按定义视为 x ∈ s ∨ x ∈ t
差：x ∈ s ∧ x ∉ t
子集：按定义 x \in s \rightarow x\in t
不属于：x ∉ t 当作否命题处理
依照命题的与，或关系处理即可
# 若要任取元素表示集合关系
s ∩ (t ∪ u) 可以分解为：rintro x ⟨xs, xt | xu⟩
s ∩ t ∪ s ∩ u \arrow : rintro x (⟨ xs,xt ⟩ | ⟨xs,xu⟩)
\. 交用\< \>包裹，逗号隔开
\. 并无需包裹，|隔开
\. ( )表示优先级
\. 默认交的优先级高于并
#证明集合相等
ext 转化为：x ∈ s ∩ t ↔ x ∈ t ∩ s
apply Subset.antisymm 转为证明相互包含
#集合列运算
`⋃ i, A i` denotes their union, and `⋂ i, A i` denotes their intersection
simp only [mem_iInter] #定义化简，简化为逻辑语言
函数的像与原像
# apply mem_image_of_mem 转化为逻辑语言
#定义逆函数：
rw[inverse]能将其改写成逻辑语言
对于有多个原像的值，会通过choose 选择一个
对于没有原像的值，会给予一个默认值
Classical.choose_spec.{u} {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (choose h)
###
重要替换方法：
theorem inverse_spec {f : α → β} (y : β) (h : ∃ x, f x = y) : f (inverse f y) = y
单射条件下要证明两个值相等只需证明两个对应的函数值相等
数学归纳法:
induction' n with n ih
--分成两个分支: 对于0成立;n成立时n+1成立
此时rw[fac]会用递推公式展开
==--在这一部分 自然数要被当作后继理解==
induction' n using Nat.strong_induction_on with n ih
--强数学归纳 ih此处为小于n的都成立
对于有限集合的归纳
induction' s using Finset.induction_on with a s ans ih
--归纳,先证明空集成立, 再对于一个已经正好的集合和一个新加的元素后依然成立
simp [Finset.prod_insert ans, prime_p.dvd_mul] at h₀ h₁
rw [mem_insert]
对添加新元素的连乘\包含关系进行化简
**连乘在空集中循环
其他细节
have Bpos : 0 < B :=by apply lt_of_le_of_lt (abs_nonneg _) (h₀ N₀ (le_refl _))
--用括号表示apply 的定理需要的两个参数, 在定理后加下划线表示用该定理自动推导出参数的形式
--N₀ (le_refl _)表示h₀需要的两个参数
--括号也表示了参数的优先级
change |a - b| / 2 > 0
--change 将目标替换为一个等价的表达式
处理极限过程 Filter
filter_upwards 解包