harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Tree/Basic.lean
theorem numLeaves_pos (x : Tree α) : 0 < x.numLeaves

Proof state:
α : Type u
x : Tree α
⊢ 0 < x.numLeaves

Tactic:
rw [numLeaves_eq_numNodes_succ]

Result:
α : Type u
x : Tree α
⊢ 0 < x.numNodes + 1

Proof state:
α : Type u
x : Tree α
⊢ 0 < x.numNodes + 1

Tactic:
exact x.numNodes.zero_lt_succ

Result:
no goals
-- Mathlib/NumberTheory/Pell.lean
theorem x_zpow_pos {a : Solution₁ d} (hax : 0 < a.x) (n : ℤ) : 0 < (a ^ n).x

Proof state:
case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
⊢ 0 < (a ^ (n + 1))⁻¹.x

Tactic:
exact x_pow_pos hax (n + 1)

Result:
no goals

Proof state:
case ofNat
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
⊢ 0 < (a ^ Int.ofNat n).x

Tactic:
rw [Int.ofNat_eq_coe, zpow_natCast]

Result:
case ofNat
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
⊢ 0 < (a ^ n).x

Proof state:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℤ
⊢ 0 < (a ^ n).x

Tactic:
cases n with
| ofNat n =>
  rw [Int.ofNat_eq_coe, zpow_natCast]
  exact x_pow_pos hax n
| negSucc n =>
  rw [zpow_negSucc]
  exact x_pow_pos hax (n + 1)

Result:
no goals

Proof state:
case ofNat
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
⊢ 0 < (a ^ n).x

Tactic:
exact x_pow_pos hax n

Result:
no goals

Proof state:
case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
⊢ 0 < (a ^ Int.negSucc n).x

Tactic:
rw [zpow_negSucc]

Result:
case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
⊢ 0 < (a ^ (n + 1))⁻¹.x
-- Mathlib/ModelTheory/Basic.lean
theorem comp_injective (h : N ↪[L] P) :
    Function.Injective (h.comp : (M ↪[L] N) →  (M ↪[L] P))

Proof state:
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ↪[L] P
⊢ Function.Injective h.comp

Tactic:
intro f g hfg

Result:
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ↪[L] P
f g : M ↪[L] N
hfg : h.comp f = h.comp g
⊢ f = g

Proof state:
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ↪[L] P
f g : M ↪[L] N
hfg : h.comp f = h.comp g
⊢ f = g

Tactic:
ext x

Result:
case h
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ↪[L] P
f g : M ↪[L] N
hfg : h.comp f = h.comp g
x : M
⊢ f x = g x

Proof state:
case h
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ↪[L] P
f g : M ↪[L] N
hfg : h.comp f = h.comp g
x : M
⊢ f x = g x

Tactic:
exact h.injective (DFunLike.congr_fun hfg x)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem back?_mapIdx {l : Vector α n} {f : Nat → α → β} :
    (mapIdx f l).back? = (l.back?).map (f (l.size - 1))

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : Nat → α → β
⊢ (mapIdx f l).back? = Option.map (f (l.size - 1)) l.back?

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l : Array α
⊢ (mapIdx f { toArray := l, size_toArray := ⋯ }).back? =
    Option.map (f ({ toArray := l, size_toArray := ⋯ }.size - 1)) { toArray := l, size_toArray := ⋯ }.back?

Proof state:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l : Array α
⊢ (mapIdx f { toArray := l, size_toArray := ⋯ }).back? =
    Option.map (f ({ toArray := l, size_toArray := ⋯ }.size - 1)) { toArray := l, size_toArray := ⋯ }.back?

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem isPeriodicPt_mul_iff_pow_eq_one (x : G) : IsPeriodicPt (x * ·) n 1 ↔ x ^ n = 1

Proof state:
G : Type u_1
inst✝ : Monoid G
n : ℕ
x : G
⊢ (fun x_1 => x ^ n * x_1) 1 = 1 ↔ x ^ n = 1

Tactic:
beta_reduce

Result:
G : Type u_1
inst✝ : Monoid G
n : ℕ
x : G
⊢ x ^ n * 1 = 1 ↔ x ^ n = 1

Proof state:
G : Type u_1
inst✝ : Monoid G
n : ℕ
x : G
⊢ IsPeriodicPt (fun x_1 => x * x_1) n 1 ↔ x ^ n = 1

Tactic:
rw [IsPeriodicPt, IsFixedPt, mul_left_iterate]

Result:
G : Type u_1
inst✝ : Monoid G
n : ℕ
x : G
⊢ (fun x_1 => x ^ n * x_1) 1 = 1 ↔ x ^ n = 1

Proof state:
G : Type u_1
inst✝ : Monoid G
n : ℕ
x : G
⊢ x ^ n * 1 = 1 ↔ x ^ n = 1

Tactic:
rw [mul_one]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean
theorem chromaticNumber_pathGraph (n : ℕ) (h : 2 ≤ n) :
    (pathGraph n).chromaticNumber = 2

Proof state:
case a
n : ℕ
h : 2 ≤ n
hc : (pathGraph n).Colorable (Fintype.card Bool)
⊢ (pathGraph n).chromaticNumber ≤ 2

Tactic:
exact hc.chromaticNumber_le

Result:
no goals

Proof state:
case a
n : ℕ
h : 2 ≤ n
hc : (pathGraph n).Colorable (Fintype.card Bool)
⊢ 2 ≤ (pathGraph n).chromaticNumber

Tactic:
have hadj : (pathGraph n).Adj ⟨0, Nat.zero_lt_of_lt h⟩ ⟨1, h⟩ := by simp [pathGraph_adj]

Result:
case a
n : ℕ
h : 2 ≤ n
hc : (pathGraph n).Colorable (Fintype.card Bool)
hadj : (pathGraph n).Adj ⟨0, ⋯⟩ ⟨1, h⟩
⊢ 2 ≤ (pathGraph n).chromaticNumber

Proof state:
case a
n : ℕ
h : 2 ≤ n
hc : (pathGraph n).Colorable (Fintype.card Bool)
hadj : (pathGraph n).Adj ⟨0, ⋯⟩ ⟨1, h⟩
⊢ 2 ≤ (pathGraph n).chromaticNumber

Tactic:
exact two_le_chromaticNumber_of_adj hadj

Result:
no goals

Proof state:
n : ℕ
h : 2 ≤ n
hc : (pathGraph n).Colorable (Fintype.card Bool)
⊢ (pathGraph n).chromaticNumber = 2

Tactic:
apply le_antisymm

Result:
case a
n : ℕ
h : 2 ≤ n
hc : (pathGraph n).Colorable (Fintype.card Bool)
⊢ (pathGraph n).chromaticNumber ≤ 2

case a
n : ℕ
h : 2 ≤ n
hc : (pathGraph n).Colorable (Fintype.card Bool)
⊢ 2 ≤ (pathGraph n).chromaticNumber

Proof state:
n : ℕ
h : 2 ≤ n
hc : (pathGraph n).Colorable (Fintype.card Bool)
⊢ (pathGraph n).Adj ⟨0, ⋯⟩ ⟨1, h⟩

Tactic:
simp [pathGraph_adj]

Result:
no goals

Proof state:
n : ℕ
h : 2 ≤ n
⊢ (pathGraph n).chromaticNumber = 2

Tactic:
have hc := (pathGraph.bicoloring n).colorable

Result:
n : ℕ
h : 2 ≤ n
hc : (pathGraph n).Colorable (Fintype.card Bool)
⊢ (pathGraph n).chromaticNumber = 2
-- Mathlib/Algebra/DirectSum/LinearMap.lean
/-- The trace of an endomorphism of a direct sum is the sum of the traces on each component.

Note that it is important the statement gives the user definitional control over `p` since the
_type_ of the term `trace R p (f.restrict hp')` depends on `p`. -/
lemma trace_eq_sum_trace_restrict_of_eq_biSup
    [∀ i, Module.Finite R (N i)] [∀ i, Module.Free R (N i)]
    (s : Finset ι) (h : iSupIndep <| fun i : s ↦ N i)
    {f : Module.End R M} (hf : ∀ i, MapsTo f (N i) (N i))
    (p : Submodule R M) (hp : p = ⨆ i ∈ s, N i)
    (hp' : MapsTo f p p := hp ▸ mapsTo_biSup_of_mapsTo (s : Set ι) hf) :
    trace R p (f.restrict hp') = ∑ i ∈ s, trace R (N i) (f.restrict (hf i))

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : ι → Submodule R M
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Module.Free R ↥(N i)
s : Finset ι
h : iSupIndep fun i => N ↑i
f : Module.End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : optParam (MapsTo ⇑f ↑p ↑p) ⋯
N' : { x // x ∈ s } → Submodule R ↥p := fun i => Submodule.comap p.subtype (N ↑i)
⊢ (trace R ↥p) (restrict f hp') = ∑ i ∈ s, (trace R ↥(N i)) (restrict f ⋯)

Tactic:
replace h : IsInternal N' := hp ▸ isInternal_biSup_submodule_of_iSupIndep (s : Set ι) h

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : ι → Submodule R M
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Module.Free R ↥(N i)
s : Finset ι
f : Module.End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : optParam (MapsTo ⇑f ↑p ↑p) ⋯
N' : { x // x ∈ s } → Submodule R ↥p := fun i => Submodule.comap p.subtype (N ↑i)
h : IsInternal N'
⊢ (trace R ↥p) (restrict f hp') = ∑ i ∈ s, (trace R ↥(N i)) (restrict f ⋯)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : ι → Submodule R M
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Module.Free R ↥(N i)
s : Finset ι
h : iSupIndep fun i => N ↑i
f : Module.End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : optParam (MapsTo ⇑f ↑p ↑p) ⋯
⊢ (trace R ↥p) (restrict f hp') = ∑ i ∈ s, (trace R ↥(N i)) (restrict f ⋯)

Tactic:
let N' : s → Submodule R p := fun i ↦ (N i).comap p.subtype

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : ι → Submodule R M
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Module.Free R ↥(N i)
s : Finset ι
h : iSupIndep fun i => N ↑i
f : Module.End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : optParam (MapsTo ⇑f ↑p ↑p) ⋯
N' : { x // x ∈ s } → Submodule R ↥p := fun i => Submodule.comap p.subtype (N ↑i)
⊢ (trace R ↥p) (restrict f hp') = ∑ i ∈ s, (trace R ↥(N i)) (restrict f ⋯)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_size_eq_size {l} :
    (filterMap f l).size = l.size ↔ ∀ a, a ∈ l → (f a).isSome

Proof state:
case mk
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
toList✝ : List α✝¹
⊢ (filterMap f { toList := toList✝ }).size = { toList := toList✝ }.size ↔
    ∀ (a : α✝¹), a ∈ { toList := toList✝ } → (f a).isSome = true

Tactic:
simp [List.filterMap_length_eq_length]

Result:
no goals

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
l : Array α✝¹
⊢ (filterMap f l).size = l.size ↔ ∀ (a : α✝¹), a ∈ l → (f a).isSome = true

Tactic:
cases l

Result:
case mk
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
toList✝ : List α✝¹
⊢ (filterMap f { toList := toList✝ }).size = { toList := toList✝ }.size ↔
    ∀ (a : α✝¹), a ∈ { toList := toList✝ } → (f a).isSome = true
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.closure_inter_eq_self_of_subset (hI : M.Indep I) (hJI : J ⊆ I) :
    M.closure J ∩ I = J

Proof state:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊆ I
hJ : M.Indep J
⊢ M.closure J ∩ I = J

Tactic:
rw [subset_antisymm_iff, and_iff_left (subset_inter (M.subset_closure _) hJI)]

Result:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊆ I
hJ : M.Indep J
⊢ M.closure J ∩ I ⊆ J

Proof state:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊆ I
⊢ M.closure J ∩ I = J

Tactic:
have hJ := hI.subset hJI

Result:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊆ I
hJ : M.Indep J
⊢ M.closure J ∩ I = J

Proof state:
case intro
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊆ I
hJ : M.Indep J
e : α
heJ : e ∈ M.closure J
heI : e ∈ I
⊢ e ∈ J

Tactic:
exact hJ.isBasis_closure.mem_of_insert_indep heJ (hI.subset (insert_subset heI hJI))

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊆ I
hJ : M.Indep J
⊢ M.closure J ∩ I ⊆ J

Tactic:
rintro e ⟨heJ, heI⟩

Result:
case intro
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊆ I
hJ : M.Indep J
e : α
heJ : e ∈ M.closure J
heI : e ∈ I
⊢ e ∈ J
-- Mathlib/CategoryTheory/MorphismProperty/Composition.lean
lemma eqToHom (W : MorphismProperty C) [W.ContainsIdentities] {x y : C} (h : x = y) :
    W (eqToHom h)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.ContainsIdentities
x : C
⊢ W (CategoryTheory.eqToHom ⋯)

Tactic:
rw [eqToHom_refl]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.ContainsIdentities
x : C
⊢ W (𝟙 x)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.ContainsIdentities
x : C
⊢ W (𝟙 x)

Tactic:
exact id_mem x

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.ContainsIdentities
x y : C
h : x = y
⊢ W (CategoryTheory.eqToHom h)

Tactic:
subst h

Result:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.ContainsIdentities
x : C
⊢ W (CategoryTheory.eqToHom ⋯)
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
@[simp]
lemma valuation_ratCast (q : ℚ) : valuation (q : ℚ_[p]) = padicValRat p q

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ (↑q).valuation = padicValRat p q

Tactic:
rcases eq_or_ne q 0 with rfl | hq

Result:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (↑0).valuation = padicValRat p 0

case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ (↑q).valuation = padicValRat p q

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ (↑q).valuation = padicValRat p q

Tactic:
refine neg_injective ((zpow_right_strictMono₀ (mod_cast hp.out.one_lt)).injective
  <| (norm_eq_zpow_neg_valuation (mod_cast hq)).symm.trans ?_)

Result:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ‖↑q‖ = ↑p ^ (-padicValRat p q)

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ‖↑q‖ = ↑p ^ (-padicValRat p q)

Tactic:
rw [padicNormE.eq_padicNorm, ← Rat.cast_natCast, ← Rat.cast_zpow, Rat.cast_inj]

Result:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ padicNorm p q = ↑p ^ (-padicValRat p q)

Proof state:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (↑0).valuation = padicValRat p 0

Tactic:
simp only [Rat.cast_zero, valuation_zero, padicValRat.zero]

Result:
no goals

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ padicNorm p q = ↑p ^ (-padicValRat p q)

Tactic:
exact padicNorm.eq_zpow_of_nonzero hq

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem card_biUnion_le [DecidableEq β] {s : Finset α} {t : α → Finset β} :
    #(s.biUnion t) ≤ ∑ a ∈ s, #(t a) :=
  haveI := Classical.decEq α
  Finset.induction_on s (by simp) fun a s has ih =>
    calc
      #((insert a s).biUnion t) ≤ #(t a) + #(s.biUnion t)

Proof state:
α : Type u_3
β : Type u_4
inst✝ : DecidableEq β
s✝ : Finset α
t : α → Finset β
this : DecidableEq α
a : α
s : Finset α
has : a ∉ s
ih : #(s.biUnion t) ≤ ∑ a ∈ s, #(t a)
⊢ #(t a) + #(s.biUnion t) ≤ #(t a) + ∑ x ∈ s, #(t x)

Tactic:
exact Nat.add_le_add_left ih _

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝ : DecidableEq β
s✝ : Finset α
t : α → Finset β
this : DecidableEq α
a : α
s : Finset α
has : a ∉ s
ih : #(s.biUnion t) ≤ ∑ a ∈ s, #(t a)
⊢ #(t a ∪ s.biUnion t) ≤ #(t a) + #(s.biUnion t)

Tactic:
exact card_union_le ..

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝ : DecidableEq β
s✝ : Finset α
t : α → Finset β
this : DecidableEq α
a : α
s : Finset α
has : a ∉ s
ih : #(s.biUnion t) ≤ ∑ a ∈ s, #(t a)
⊢ #(t a) + #(s.biUnion t) ≤ ∑ a ∈ insert a s, #(t a)

Tactic:
rw [sum_insert has]

Result:
α : Type u_3
β : Type u_4
inst✝ : DecidableEq β
s✝ : Finset α
t : α → Finset β
this : DecidableEq α
a : α
s : Finset α
has : a ∉ s
ih : #(s.biUnion t) ≤ ∑ a ∈ s, #(t a)
⊢ #(t a) + #(s.biUnion t) ≤ #(t a) + ∑ x ∈ s, #(t x)

Proof state:
α : Type u_3
β : Type u_4
inst✝ : DecidableEq β
s✝ : Finset α
t : α → Finset β
this : DecidableEq α
a : α
s : Finset α
has : a ∉ s
ih : #(s.biUnion t) ≤ ∑ a ∈ s, #(t a)
⊢ #((insert a s).biUnion t) ≤ #(t a) + #(s.biUnion t)

Tactic:
rw [biUnion_insert]

Result:
α : Type u_3
β : Type u_4
inst✝ : DecidableEq β
s✝ : Finset α
t : α → Finset β
this : DecidableEq α
a : α
s : Finset α
has : a ∉ s
ih : #(s.biUnion t) ≤ ∑ a ∈ s, #(t a)
⊢ #(t a ∪ s.biUnion t) ≤ #(t a) + #(s.biUnion t)

Proof state:
α : Type u_3
β : Type u_4
inst✝ : DecidableEq β
s : Finset α
t : α → Finset β
this : DecidableEq α
⊢ #(∅.biUnion t) ≤ ∑ a ∈ ∅, #(t a)

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem Function.Injective.swap_apply
    [DecidableEq α] [DecidableEq β] {f : α → β} (hf : Function.Injective f) (x y z : α) :
    Equiv.swap (f x) (f y) (f z) = f (Equiv.swap x y z)

Proof state:
case pos
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
hx : ¬z = x
hy : z = y
⊢ (Equiv.swap (f x) (f y)) (f z) = f ((Equiv.swap x y) z)

Tactic:
simp [hy]

Result:
no goals

Proof state:
case neg
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
hx : ¬z = x
⊢ (Equiv.swap (f x) (f y)) (f z) = f ((Equiv.swap x y) z)

Tactic:
by_cases hy : z = y

Result:
case pos
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
hx : ¬z = x
hy : z = y
⊢ (Equiv.swap (f x) (f y)) (f z) = f ((Equiv.swap x y) z)

case neg
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
hx : ¬z = x
hy : ¬z = y
⊢ (Equiv.swap (f x) (f y)) (f z) = f ((Equiv.swap x y) z)

Proof state:
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
⊢ (Equiv.swap (f x) (f y)) (f z) = f ((Equiv.swap x y) z)

Tactic:
by_cases hx : z = x

Result:
case pos
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
hx : z = x
⊢ (Equiv.swap (f x) (f y)) (f z) = f ((Equiv.swap x y) z)

case neg
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
hx : ¬z = x
⊢ (Equiv.swap (f x) (f y)) (f z) = f ((Equiv.swap x y) z)

Proof state:
case pos
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
hx : z = x
⊢ (Equiv.swap (f x) (f y)) (f z) = f ((Equiv.swap x y) z)

Tactic:
simp [hx]

Result:
no goals

Proof state:
case neg
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
hx : ¬z = x
hy : ¬z = y
⊢ (Equiv.swap (f x) (f y)) (f z) = f ((Equiv.swap x y) z)

Tactic:
rw [Equiv.swap_apply_of_ne_of_ne hx hy, Equiv.swap_apply_of_ne_of_ne (hf.ne hx) (hf.ne hy)]

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_strictMono : StrictMono exp := fun x y h => by
  rw [← sub_add_cancel y x, Real.exp_add]
  exact (lt_mul_iff_one_lt_left (exp_pos _)).2
      (lt_of_lt_of_le (by linarith) (add_one_le_exp_of_nonneg (by linarith)))

Proof state:
x y : ℝ
h : x < y
⊢ rexp x < rexp (y - x) * rexp x

Tactic:
exact (lt_mul_iff_one_lt_left (exp_pos _)).2
    (lt_of_lt_of_le (by linarith) (add_one_le_exp_of_nonneg (by linarith)))

Result:
no goals

Proof state:
x y : ℝ
h : x < y
⊢ 1 < y - x + 1

Tactic:
linarith

Result:
no goals

Proof state:
x y : ℝ
h : x < y
⊢ 0 ≤ y - x

Tactic:
linarith

Result:
no goals

Proof state:
x y : ℝ
h : x < y
⊢ rexp x < rexp y

Tactic:
rw [← sub_add_cancel y x, Real.exp_add]

Result:
x y : ℝ
h : x < y
⊢ rexp x < rexp (y - x) * rexp x
-- Mathlib/RingTheory/Polynomial/IrreducibleRing.lean
theorem Polynomial.Monic.irreducible_of_irreducible_map_of_isPrime_nilradical
    {R S : Type*} [CommRing R] [(nilradical R).IsPrime] [CommRing S] [IsDomain S]
    (φ : R →+* S) (f : R[X]) (hm : f.Monic) (hi : Irreducible (f.map φ)) : Irreducible f

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (b.coeff i)
hc : f.leadingCoeff = (a * b).coeff f.natDegree
⊢ IsUnit (-(a.coeff f.natDegree * b.coeff 0))

Tactic:
rw [hm, coeff_mul, Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun i j ↦ a.coeff i * b.coeff j,
  Finset.sum_range_succ, ← sub_eq_iff_eq_add, Nat.sub_self] at hc

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (b.coeff i)
hc : 1 - a.coeff f.natDegree * b.coeff 0 = ∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x)
⊢ IsUnit (-(a.coeff f.natDegree * b.coeff 0))
-- Mathlib/NumberTheory/NumberField/Basic.lean
theorem mem_span_integralBasis {x : K} :
    x ∈ Submodule.span ℤ (Set.range (integralBasis K)) ↔ x ∈ (algebraMap (𝓞 K) K).range

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ x ∈ Submodule.span ℤ (Set.range ⇑(integralBasis K)) ↔ x ∈ (algebraMap (𝓞 K) K).range

Tactic:
rw [integralBasis, Basis.localizationLocalization_span, LinearMap.mem_range,
    IsScalarTower.coe_toAlgHom', RingHom.mem_range]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem getElem_drop' (L : List α) {i j : Nat} (h : i + j < L.length) :
    L[i + j] = (L.drop i)[j]'(lt_length_drop L h)

Proof state:
α : Type u_1
L : List α
i j : Nat
h : i + j < L.length
⊢ L[i + j] = (drop i L)[j]

Tactic:
have : i ≤ L.length := Nat.le_trans (Nat.le_add_right _ _) (Nat.le_of_lt h)

Result:
α : Type u_1
L : List α
i j : Nat
h : i + j < L.length
this : i ≤ L.length
⊢ L[i + j] = (drop i L)[j]

Proof state:
case h₁
α : Type u_1
L : List α
i j : Nat
h : i + j < L.length
this : i ≤ L.length
⊢ (take i L).length ≤ i + j

Tactic:
simp [Nat.min_eq_left this, Nat.le_add_right]

Result:
no goals

Proof state:
α : Type u_1
L : List α
i j : Nat
h : i + j < L.length
this : i ≤ L.length
⊢ L[i + j] = (drop i L)[j]

Tactic:
rw [getElem_of_eq (take_append_drop i L).symm h, getElem_append_right]

Result:
α : Type u_1
L : List α
i j : Nat
h : i + j < L.length
this : i ≤ L.length
⊢ (drop i L)[i + j - (take i L).length] = (drop i L)[j]

case h₁
α : Type u_1
L : List α
i j : Nat
h : i + j < L.length
this : i ≤ L.length
⊢ (take i L).length ≤ i + j

Proof state:
α : Type u_1
L : List α
i j : Nat
h : i + j < L.length
this : i ≤ L.length
⊢ (drop i L)[i + j - (take i L).length] = (drop i L)[j]

Tactic:
simp [Nat.min_eq_left this, Nat.add_sub_cancel_left]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem erase_insert_eq_erase (s : Finset α) (a : α) : (insert a s).erase a = s.erase a :=
  ext fun x => by
    simp +contextual only [mem_erase, mem_insert, and_congr_right_iff,
      false_or, iff_self, imp_true_iff]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a x : α
⊢ x ∈ (insert a s).erase a ↔ x ∈ s.erase a

Tactic:
simp +contextual only [mem_erase, mem_insert, and_congr_right_iff,
  false_or, iff_self, imp_true_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem Module.finite_of_rank_eq_nat [Module.Free R M] {n : ℕ} (h : Module.rank R M = n) :
    Module.Finite R M

Proof state:
case intro.mk
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
n : ℕ
h : Module.rank R M = ↑n
a✝ : Nontrivial R
ι : Type v
b : Basis ι R M
this : Finite ι
⊢ Module.Finite R M

Tactic:
exact Module.Finite.of_basis b

Result:
no goals

Proof state:
case intro.mk
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
n : ℕ
h : Module.rank R M = ↑n
a✝ : Nontrivial R
ι : Type v
b : Basis ι R M
⊢ Module.Finite R M

Tactic:
have := mk_lt_aleph0_iff.mp <|
  b.linearIndependent.cardinal_le_rank |>.trans_eq h |>.trans_lt <| nat_lt_aleph0 n

Result:
case intro.mk
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
n : ℕ
h : Module.rank R M = ↑n
a✝ : Nontrivial R
ι : Type v
b : Basis ι R M
this : Finite ι
⊢ Module.Finite R M

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
n : ℕ
h : Module.rank R M = ↑n
a✝ : Nontrivial R
⊢ Module.Finite R M

Tactic:
obtain ⟨⟨ι, b⟩⟩ := Module.Free.exists_basis (R := R) (M := M)

Result:
case intro.mk
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
n : ℕ
h : Module.rank R M = ↑n
a✝ : Nontrivial R
ι : Type v
b : Basis ι R M
⊢ Module.Finite R M

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
n : ℕ
h : Module.rank R M = ↑n
⊢ Module.Finite R M

Tactic:
nontriviality R

Result:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
n : ℕ
h : Module.rank R M = ↑n
a✝ : Nontrivial R
⊢ Module.Finite R M