harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem erase_eq_self_iff [LawfulBEq α] {l : Array α} : l.erase a = l ↔ a ∉ l

Proof state:
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
l : Array α
⊢ (∀ (a_1 : α), a_1 ∈ l → ¬(a_1 == a) = true) ↔ ¬a ∈ l

Tactic:
simp [forall_mem_ne']

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
l : Array α
⊢ l.erase a = l ↔ ¬a ∈ l

Tactic:
rw [erase_eq_eraseP', eraseP_eq_self_iff]

Result:
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
l : Array α
⊢ (∀ (a_1 : α), a_1 ∈ l → ¬(a_1 == a) = true) ↔ ¬a ∈ l
-- Mathlib/LinearAlgebra/TensorProduct/Submodule.lean
theorem mulMap_comm_of_commute (hc : ∀ (m : M) (n : N), Commute m.1 n.1) :
    mulMap N M = mulMap M N ∘ₗ TensorProduct.comm R N M

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
hc : ∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n
n : ↥N
m : ↥M
⊢ (N.mulMap M) (n ⊗ₜ[R] m) = (M.mulMap N ∘ₗ ↑(TensorProduct.comm R ↥N ↥M)) (n ⊗ₜ[R] m)

Tactic:
simp_rw [LinearMap.comp_apply, LinearEquiv.coe_coe, TensorProduct.comm_tmul, mulMap_tmul]

Result:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
hc : ∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n
n : ↥N
m : ↥M
⊢ ↑n * ↑m = ↑m * ↑n

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
hc : ∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n
n : ↥N
m : ↥M
⊢ ↑n * ↑m = ↑m * ↑n

Tactic:
exact (hc m n).symm

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
hc : ∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n
⊢ N.mulMap M = M.mulMap N ∘ₗ ↑(TensorProduct.comm R ↥N ↥M)

Tactic:
refine TensorProduct.ext' fun n m ↦ ?_

Result:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
hc : ∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n
n : ↥N
m : ↥M
⊢ (N.mulMap M) (n ⊗ₜ[R] m) = (M.mulMap N ∘ₗ ↑(TensorProduct.comm R ↥N ↥M)) (n ⊗ₜ[R] m)
-- Mathlib/Data/Nat/Sqrt.lean
private lemma sqrt_isSqrt (n : ℕ) : IsSqrt n (sqrt n)

Proof state:
n : ℕ
⊢ Nat.IsSqrt 0 (sqrt 0)

Tactic:
simp [IsSqrt, sqrt]

Result:
no goals

Proof state:
n : ℕ
⊢ Nat.IsSqrt 1 (sqrt 1)

Tactic:
simp [IsSqrt, sqrt]

Result:
no goals

Proof state:
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 ≤ (n + 2) / 2 * ((n + 2) / 2) + (n + 2) / 2 * 2

Tactic:
refine le_trans (Nat.le_of_eq (div_add_mod' (n + 2) 2).symm) ?_

Result:
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ (n + 2) / 2 * 2 + (n + 2) % 2 ≤ (n + 2) / 2 * ((n + 2) / 2) + (n + 2) / 2 * 2

Proof state:
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ Nat.IsSqrt (n + 2) (n + 2).sqrt

Tactic:
simp only [IsSqrt, sqrt, h, ite_false]

Result:
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ sqrt.iter (n + 2) ((n + 2) / 2) * sqrt.iter (n + 2) ((n + 2) / 2) ≤ n + 2 ∧
    n + 2 < (sqrt.iter (n + 2) ((n + 2) / 2) + 1) * (sqrt.iter (n + 2) ((n + 2) / 2) + 1)

Proof state:
n✝ n : ℕ
⊢ Nat.IsSqrt (n + 2) (n + 2).sqrt

Tactic:
have h : ¬ (n + 2) ≤ 1 := by simp

Result:
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ Nat.IsSqrt (n + 2) (n + 2).sqrt

Proof state:
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 < (n + 2) / 2 * ((n + 2) / 2) + (n + 2) / 2 + (n + 2) / 2 + 1

Tactic:
rw [Nat.lt_add_one_iff, Nat.add_assoc, ← Nat.mul_two]

Result:
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 ≤ (n + 2) / 2 * ((n + 2) / 2) + (n + 2) / 2 * 2

Proof state:
case refine_2
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ 1 ≤ n / 2 * (n / 2) + n / 2 + n / 2 + 1

Tactic:
exact Nat.le_add_left _ _

Result:
no goals

Proof state:
n✝ n : ℕ
⊢ ¬n + 2 ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n % 2 ≤ (n + 2) / 2 * ((n + 2) / 2)

Tactic:
simp only [Nat.zero_lt_two, add_div_right, succ_mul_succ]

Result:
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n % 2 ≤ n / 2 * (n / 2) + n / 2 + n / 2 + 1

Proof state:
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ (n + 2) / 2 * 2 + (n + 2) % 2 ≤ (n + 2) / 2 * ((n + 2) / 2) + (n + 2) / 2 * 2

Tactic:
rw [Nat.add_comm, Nat.add_le_add_iff_right, add_mod_right]

Result:
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n % 2 ≤ (n + 2) / 2 * ((n + 2) / 2)

Proof state:
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ sqrt.iter (n + 2) ((n + 2) / 2) * sqrt.iter (n + 2) ((n + 2) / 2) ≤ n + 2 ∧
    n + 2 < (sqrt.iter (n + 2) ((n + 2) / 2) + 1) * (sqrt.iter (n + 2) ((n + 2) / 2) + 1)

Tactic:
refine ⟨sqrt.iter_sq_le _ _, sqrt.lt_iter_succ_sq _ _ ?_⟩

Result:
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 < ((n + 2) / 2 + 1) * ((n + 2) / 2 + 1)

Proof state:
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n % 2 ≤ n / 2 * (n / 2) + n / 2 + n / 2 + 1

Tactic:
refine le_trans (b := 1) ?_ ?_

Result:
case refine_1
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n % 2 ≤ 1

case refine_2
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ 1 ≤ n / 2 * (n / 2) + n / 2 + n / 2 + 1

Proof state:
case refine_1
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n % 2 ≤ 1

Tactic:
exact (lt_succ.1 <| mod_lt n Nat.zero_lt_two)

Result:
no goals

Proof state:
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 < ((n + 2) / 2 + 1) * ((n + 2) / 2 + 1)

Tactic:
simp only [Nat.mul_add, Nat.add_mul, Nat.one_mul, Nat.mul_one, ← Nat.add_assoc]

Result:
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 < (n + 2) / 2 * ((n + 2) / 2) + (n + 2) / 2 + (n + 2) / 2 + 1
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
theorem CNF.unsat_of_convertLRAT_unsat (cnf : CNF Nat) :
    Unsatisfiable (PosFin (cnf.numLiterals + 1)) (CNF.convertLRAT cnf)
      →
    cnf.Unsat

Proof state:
case a.a
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
h2 : CNF.eval assignment (lift cnf) = true
⊢ assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray

Tactic:
simp only [Formula.formulaEntails_def, List.all_eq_true, decide_eq_true_eq]

Result:
case a.a
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
h2 : CNF.eval assignment (lift cnf) = true
⊢ ∀ (x : DefaultClause (cnf.numLiterals + 1)),
    x ∈ Formula.toList (DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray) → assignment ⊨ x
-- Mathlib/Data/Nat/PartENat.lean
theorem natCast_get {x : PartENat} (h : x.Dom) : (x.get h : PartENat) = x

Proof state:
x : PartENat
h : x.Dom
⊢ ↑(x.get h) = x

Tactic:
exact Part.ext' (iff_of_true trivial h) fun _ _ => rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem coeff_zero_eq_aeval_zero' (p : R[X]) : algebraMap R A (p.coeff 0) = aeval (0 : A) p

Proof state:
R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
⊢ (algebraMap R A) (p.coeff 0) = (aeval 0) p

Tactic:
simp [aeval_def]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem map_S (f : R →+* R') (n : ℤ) : map f (S R n) = S R' n

Proof state:
case add_two
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (S R (↑n + 1)) = S R' (↑n + 1)
ih2 : map f (S R ↑n) = S R' ↑n
⊢ map f (S R (↑n + 2)) = S R' (↑n + 2)

Tactic:
simp_rw [S_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]

Result:
no goals

Proof state:
case one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
⊢ map f (S R 1) = S R' 1

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℤ
⊢ map f (S R n) = S R' n

Tactic:
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp
| add_two n ih1 ih2 =>
  simp_rw [S_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]
| neg_add_one n ih1 ih2 =>
  simp_rw [S_sub_one, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]

Result:
no goals

Proof state:
case zero
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
⊢ map f (S R 0) = S R' 0

Tactic:
simp

Result:
no goals

Proof state:
case neg_add_one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (S R (-↑n)) = S R' (-↑n)
ih2 : map f (S R (-↑n + 1)) = S R' (-↑n + 1)
⊢ map f (S R (-↑n - 1)) = S R' (-↑n - 1)

Tactic:
simp_rw [S_sub_one, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]

Result:
no goals
-- Mathlib/Data/List/Sublists.lean
theorem sublists'Aux_eq_array_foldl (a : α) : ∀ (r₁ r₂ : List (List α)),
    sublists'Aux a r₁ r₂ = ((r₁.toArray).foldl (init := r₂.toArray)
      (fun r l => r.push (a :: l))).toList

Proof state:
α : Type u
a : α
r₁ r₂ : List (List α)
⊢ ∀ (x : Array (List α)) (y : List α), (fun r l => r ++ [a :: l]) x.toList y = ((fun r l => r.push (a :: l)) x y).toList

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
a : α
r₁ r₂ : List (List α)
⊢ Array.foldl (fun r l => r ++ [a :: l]) r₂ { toList := r₁ } =
    (Array.foldl (fun r l => r.push (a :: l)) r₂.toArray r₁.toArray).toList

Tactic:
have := List.foldl_hom Array.toList (fun r l => r.push (a :: l))
  (fun r l => r ++ [a :: l]) r₁ r₂.toArray (by simp)

Result:
α : Type u
a : α
r₁ r₂ : List (List α)
this : foldl (fun r l => r ++ [a :: l]) r₂.toArray.toList r₁ = (foldl (fun r l => r.push (a :: l)) r₂.toArray r₁).toList
⊢ Array.foldl (fun r l => r ++ [a :: l]) r₂ { toList := r₁ } =
    (Array.foldl (fun r l => r.push (a :: l)) r₂.toArray r₁.toArray).toList

Proof state:
α : Type u
a : α
r₁ r₂ : List (List α)
this : foldl (fun r l => r ++ [a :: l]) r₂.toArray.toList r₁ = (foldl (fun r l => r.push (a :: l)) r₂.toArray r₁).toList
⊢ Array.foldl (fun r l => r ++ [a :: l]) r₂ { toList := r₁ } =
    (Array.foldl (fun r l => r.push (a :: l)) r₂.toArray r₁.toArray).toList

Tactic:
simpa using this

Result:
no goals

Proof state:
α : Type u
a : α
r₁ r₂ : List (List α)
⊢ sublists'Aux a r₁ r₂ = (Array.foldl (fun r l => r.push (a :: l)) r₂.toArray r₁.toArray).toList

Tactic:
rw [sublists'Aux, Array.foldl_toList]

Result:
α : Type u
a : α
r₁ r₂ : List (List α)
⊢ Array.foldl (fun r l => r ++ [a :: l]) r₂ { toList := r₁ } =
    (Array.foldl (fun r l => r.push (a :: l)) r₂.toArray r₁.toArray).toList

Proof state:
α : Type u
a : α
⊢ ∀ (r₁ r₂ : List (List α)),
    sublists'Aux a r₁ r₂ = (Array.foldl (fun r l => r.push (a :: l)) r₂.toArray r₁.toArray).toList

Tactic:
intro r₁ r₂

Result:
α : Type u
a : α
r₁ r₂ : List (List α)
⊢ sublists'Aux a r₁ r₂ = (Array.foldl (fun r l => r.push (a :: l)) r₂.toArray r₁.toArray).toList
-- Mathlib/AlgebraicGeometry/Scheme.lean
@[reassoc (attr := simp)]
lemma appLE_map (e : V ≤ f ⁻¹ᵁ U) (i : op V ⟶ op V') :
    f.appLE U V e ≫ X.presheaf.map i = f.appLE U V' (i.unop.le.trans e)

Proof state:
X Y : Scheme
f : X.Hom Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op V ⟶ op V'
⊢ f.appLE U V e ≫ X.presheaf.map i = f.appLE U V' ⋯

Tactic:
rw [Hom.appLE, Category.assoc, ← Functor.map_comp]

Result:
X Y : Scheme
f : X.Hom Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op V ⟶ op V'
⊢ f.app U ≫ X.presheaf.map ((homOfLE e).op ≫ i) = f.appLE U V' ⋯

Proof state:
X Y : Scheme
f : X.Hom Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op V ⟶ op V'
⊢ f.app U ≫ X.presheaf.map ((homOfLE e).op ≫ i) = f.appLE U V' ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} {h₁} :
    getKey (m.insertIfNew k v) a h₁ =
      if h₂ : k == a ∧ ¬k ∈ m then k else getKey m a (mem_of_mem_insertIfNew' h h₁ h₂)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β k
h₁ : a ∈ m.insertIfNew k v
⊢ (m.insertIfNew k v).getKey a h₁ = if h : (k == a) = true ∧ m.contains k = false then k else m.getKey a ⋯

Tactic:
simp_to_raw using Raw₀.getKey_insertIfNew ⟨m, _⟩

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β k
h₁ : a ∈ m.insertIfNew k v
⊢ (m.insertIfNew k v).getKey a h₁ = if h₂ : (k == a) = true ∧ ¬k ∈ m then k else m.getKey a ⋯

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β k
h₁ : a ∈ m.insertIfNew k v
⊢ (m.insertIfNew k v).getKey a h₁ = if h : (k == a) = true ∧ m.contains k = false then k else m.getKey a ⋯
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem adj_iff_exists_edge {v w : V} : G.Adj v w ↔ v ≠ w ∧ ∃ e ∈ G.edgeSet, v ∈ e ∧ w ∈ e

Proof state:
case intro.intro.intro
V : Type u
G : SimpleGraph V
v w : V
hne : v ≠ w
e : Sym2 V
he : e ∈ G.edgeSet
hv : v ∈ e ∧ w ∈ e
⊢ G.Adj v w

Tactic:
rw [Sym2.mem_and_mem_iff hne] at hv

Result:
case intro.intro.intro
V : Type u
G : SimpleGraph V
v w : V
hne : v ≠ w
e : Sym2 V
he : e ∈ G.edgeSet
hv : e = s(v, w)
⊢ G.Adj v w

Proof state:
V : Type u
G : SimpleGraph V
v w : V
x✝ : G.Adj v w
⊢ s(v, w) ∈ G.edgeSet ∧ v ∈ s(v, w) ∧ w ∈ s(v, w)

Tactic:
simpa

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v w : V
⊢ G.Adj v w ↔ v ≠ w ∧ ∃ e ∈ G.edgeSet, v ∈ e ∧ w ∈ e

Tactic:
refine ⟨fun _ => ⟨G.ne_of_adj ‹_›, s(v, w), by simpa⟩, ?_⟩

Result:
V : Type u
G : SimpleGraph V
v w : V
⊢ (v ≠ w ∧ ∃ e ∈ G.edgeSet, v ∈ e ∧ w ∈ e) → G.Adj v w

Proof state:
V : Type u
G : SimpleGraph V
v w : V
⊢ (v ≠ w ∧ ∃ e ∈ G.edgeSet, v ∈ e ∧ w ∈ e) → G.Adj v w

Tactic:
rintro ⟨hne, e, he, hv⟩

Result:
case intro.intro.intro
V : Type u
G : SimpleGraph V
v w : V
hne : v ≠ w
e : Sym2 V
he : e ∈ G.edgeSet
hv : v ∈ e ∧ w ∈ e
⊢ G.Adj v w

Proof state:
case intro.intro.intro
V : Type u
G : SimpleGraph V
v w : V
hne : v ≠ w
he : s(v, w) ∈ G.edgeSet
⊢ G.Adj v w

Tactic:
rwa [mem_edgeSet] at he

Result:
no goals

Proof state:
case intro.intro.intro
V : Type u
G : SimpleGraph V
v w : V
hne : v ≠ w
e : Sym2 V
he : e ∈ G.edgeSet
hv : e = s(v, w)
⊢ G.Adj v w

Tactic:
subst e

Result:
case intro.intro.intro
V : Type u
G : SimpleGraph V
v w : V
hne : v ≠ w
he : s(v, w) ∈ G.edgeSet
⊢ G.Adj v w
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem Colorable.mono {n m : ℕ} (h : n ≤ m) (hc : G.Colorable n) : G.Colorable m :=
  ⟨G.recolorOfCardLE (by simp [h]) hc.some⟩

Proof state:
V : Type u
G : SimpleGraph V
n m : ℕ
h : n ≤ m
hc : G.Colorable n
⊢ card (Fin n) ≤ card (Fin m)

Tactic:
simp [h]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
theorem orderOf_r_one : orderOf (r 1 : DihedralGroup n) = n

Proof state:
case inl

⊢ orderOf (r 1) = 0

Tactic:
rw [orderOf_eq_zero_iff']

Result:
case inl

⊢ ∀ (n : ℕ), 0 < n → r 1 ^ n ≠ 1

Proof state:
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h2 : orderOf (r 1) = 0
⊢ False

Tactic:
exact absurd h2.symm (orderOf_pos _).ne

Result:
no goals

Proof state:
case inl

⊢ ∀ (n : ℕ), 0 < n → r 1 ^ n ≠ 1

Tactic:
intro n hn

Result:
case inl
n : ℕ
hn : 0 < n
⊢ r 1 ^ n ≠ 1

Proof state:
case inl
n : ℕ
hn : 0 < n
⊢ r 1 ^ n ≠ 1

Tactic:
rw [r_one_pow, one_def]

Result:
case inl
n : ℕ
hn : 0 < n
⊢ r ↑n ≠ r 0

Proof state:
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h1 : r ↑(orderOf (r 1)) = 1
⊢ False

Tactic:
injection h1 with h2

Result:
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h2 : ↑(orderOf (r 1)) = 0
⊢ False

Proof state:
n : ℕ
⊢ orderOf (r 1) = n

Tactic:
rcases eq_zero_or_neZero n with (rfl | hn)

Result:
case inl

⊢ orderOf (r 1) = 0

case inr
n : ℕ
hn : NeZero n
⊢ orderOf (r 1) = n

Proof state:
case inr
n : ℕ
hn : NeZero n
⊢ ¬orderOf (r 1) < n

Tactic:
intro h

Result:
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
⊢ False

Proof state:
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h1 : r 1 ^ orderOf (r 1) = 1
⊢ False

Tactic:
rw [r_one_pow] at h1

Result:
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h1 : r ↑(orderOf (r 1)) = 1
⊢ False

Proof state:
case inl
n : ℕ
hn : 0 < n
⊢ r ↑n ≠ r 0

Tactic:
apply mt r.inj

Result:
case inl
n : ℕ
hn : 0 < n
⊢ ¬↑n = 0

Proof state:
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h2 : ↑(orderOf (r 1)) = 0
⊢ False

Tactic:
rw [← ZMod.val_eq_zero, ZMod.val_natCast, Nat.mod_eq_of_lt h] at h2

Result:
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h2 : orderOf (r 1) = 0
⊢ False

Proof state:
case inr
n : ℕ
hn : NeZero n
⊢ orderOf (r 1) = n

Tactic:
apply (Nat.le_of_dvd (NeZero.pos n) <|
  orderOf_dvd_of_pow_eq_one <| @r_one_pow_n n).lt_or_eq.resolve_left

Result:
case inr
n : ℕ
hn : NeZero n
⊢ ¬orderOf (r 1) < n

Proof state:
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
⊢ False

Tactic:
have h1 : (r 1 : DihedralGroup n) ^ orderOf (r 1) = 1 := pow_orderOf_eq_one _

Result:
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h1 : r 1 ^ orderOf (r 1) = 1
⊢ False

Proof state:
case inl
n : ℕ
hn : 0 < n
⊢ ¬↑n = 0

Tactic:
simpa using hn.ne'

Result:
no goals
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem pullbackFstιToV_snd (i j : 𝒰.J) :
    pullbackFstιToV 𝒰 f g i j ≫ pullback.snd _ _ = pullback.fst _ _ ≫ pullback.snd _ _

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j : 𝒰.J
⊢ pullbackFstιToV 𝒰 f g i j ≫ pullback.snd (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) =
    pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).ι j) ≫ pullback.snd (p1 𝒰 f g) (𝒰.map i)

Tactic:
simp [pullbackFstιToV, p1]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
lemma inv_mul_eq_one_of_isUnit {n : ℕ} {a : ZMod n} (ha : IsUnit a) (b : ZMod n) :
    a⁻¹ * b = 1 ↔ a = b

Proof state:
n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
⊢ a⁻¹ * b = 1 ↔ a = b

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ H ▸ a.inv_mul_of_unit ha⟩

Result:
n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
H : a⁻¹ * b = 1
⊢ a = b

Proof state:
n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
H : a * (a⁻¹ * b) = a * 1
⊢ a = b

Tactic:
rwa [← mul_assoc, a.mul_inv_of_unit ha, one_mul, mul_one, eq_comm] at H

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem closure_image_mem_nhds_of_isUniformInducing {s : Set (α × α)} {e : α → β} (b : β)
    (he₁ : IsUniformInducing e) (he₂ : IsDenseInducing e) (hs : s ∈ 𝓤 α) :
    ∃ a, closure (e '' { a' | (a, a') ∈ s }) ∈ 𝓝 b

Proof state:
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
⊢ ∃ a, closure (e '' {a' | (a, a') ∈ s}) ∈ 𝓝 b

Tactic:
refine ⟨a, mem_of_superset ?_ (closure_mono <| image_subset _ <| UniformSpace.ball_mono hs a)⟩

Result:
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
⊢ closure (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)) ∈ 𝓝 b
-- Mathlib/Data/Sym/Card.lean
theorem card_image_diag (s : Finset α) : #(s.diag.image Sym2.mk) = #s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn Sym2.mk ↑s.diag

Tactic:
rintro ⟨x₀, x₁⟩ hx _ _ h

Result:
case mk
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
hx : (x₀, x₁) ∈ ↑s.diag
x₂✝ : α × α
a✝ : x₂✝ ∈ ↑s.diag
h : s(x₀, x₁) = Sym2.mk x₂✝
⊢ (x₀, x₁) = x₂✝

Proof state:
case mk
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
hx : (x₀, x₁) ∈ ↑s.diag
x₂✝ : α × α
a✝ : x₂✝ ∈ ↑s.diag
h : s(x₀, x₁) = Sym2.mk x₂✝
⊢ (x₀, x₁) = x₂✝

Tactic:
cases Sym2.eq.1 h

Result:
case mk.refl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
hx a✝ : (x₀, x₁) ∈ ↑s.diag
h : s(x₀, x₁) = s(x₀, x₁)
⊢ (x₀, x₁) = (x₀, x₁)

case mk.swap
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
hx : (x₀, x₁) ∈ ↑s.diag
a✝ : (x₁, x₀) ∈ ↑s.diag
h : s(x₀, x₁) = s(x₁, x₀)
⊢ (x₀, x₁) = (x₁, x₀)

Proof state:
case mk.refl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
hx a✝ : (x₀, x₁) ∈ ↑s.diag
h : s(x₀, x₁) = s(x₀, x₁)
⊢ (x₀, x₁) = (x₀, x₁)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ #(image Sym2.mk s.diag) = #s

Tactic:
rw [card_image_of_injOn, diag_card]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn Sym2.mk ↑s.diag

Proof state:
case mk.swap
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
a✝ : (x₁, x₀) ∈ ↑s.diag
h : s(x₀, x₁) = s(x₁, x₀)
hx : x₀ ∈ s ∧ x₀ = x₁
⊢ (x₀, x₁) = (x₁, x₀)

Tactic:
rw [hx.2]

Result:
no goals

Proof state:
case mk.swap
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
hx : (x₀, x₁) ∈ ↑s.diag
a✝ : (x₁, x₀) ∈ ↑s.diag
h : s(x₀, x₁) = s(x₁, x₀)
⊢ (x₀, x₁) = (x₁, x₀)

Tactic:
simp only [mem_coe, mem_diag] at hx

Result:
case mk.swap
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
a✝ : (x₁, x₀) ∈ ↑s.diag
h : s(x₀, x₁) = s(x₁, x₀)
hx : x₀ ∈ s ∧ x₀ = x₁
⊢ (x₀, x₁) = (x₁, x₀)
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem π_comp_cokernelIsoOfEq_inv {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) :
    cokernel.π _ ≫ (cokernelIsoOfEq h).inv = cokernel.π _

Proof state:
case refl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ inst✝ : HasCokernel f
⊢ cokernel.π f ≫ (cokernelIsoOfEq ⋯).inv = cokernel.π f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : HasCokernel g
h : f = g
⊢ cokernel.π g ≫ (cokernelIsoOfEq h).inv = cokernel.π f

Tactic:
cases h

Result:
case refl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ inst✝ : HasCokernel f
⊢ cokernel.π f ≫ (cokernelIsoOfEq ⋯).inv = cokernel.π f
-- Mathlib/Topology/Sheaves/Stalks.lean
theorem stalkSpecializes_comp {C : Type*} [Category C] [Limits.HasColimits C] {X : TopCat}
    (F : X.Presheaf C) {x y z : X} (h : x ⤳ y) (h' : y ⤳ z) :
    F.stalkSpecializes h' ≫ F.stalkSpecializes h = F.stalkSpecializes (h.trans h')

Proof state:
C : Type u_3
inst✝¹ : Category.{u_4, u_3} C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x y z : ↑X
h : x ⤳ y
h' : y ⤳ z
⊢ F.stalkSpecializes h' ≫ F.stalkSpecializes h = F.stalkSpecializes ⋯

Tactic:
ext

Result:
case ih
C : Type u_3
inst✝¹ : Category.{u_4, u_3} C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x y z : ↑X
h : x ⤳ y
h' : y ⤳ z
U✝ : Opens ↑X
hxU✝ : z ∈ U✝
⊢ F.germ U✝ z hxU✝ ≫ F.stalkSpecializes h' ≫ F.stalkSpecializes h = F.germ U✝ z hxU✝ ≫ F.stalkSpecializes ⋯

Proof state:
case ih
C : Type u_3
inst✝¹ : Category.{u_4, u_3} C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x y z : ↑X
h : x ⤳ y
h' : y ⤳ z
U✝ : Opens ↑X
hxU✝ : z ∈ U✝
⊢ F.germ U✝ z hxU✝ ≫ F.stalkSpecializes h' ≫ F.stalkSpecializes h = F.germ U✝ z hxU✝ ≫ F.stalkSpecializes ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Injectivity.lean
/-- If the `LSeries` of `f` and of `g` both converge somewhere, then they are equal if and only
if `f n = g n` whenever `n ≠ 0`. -/
lemma LSeries_eq_iff_of_abscissaOfAbsConv_lt_top {f g : ℕ → ℂ} (hf : abscissaOfAbsConv f < ⊤)
    (hg : abscissaOfAbsConv g < ⊤) :
    LSeries f = LSeries g ↔ ∀ n ≠ 0, f n = g n

Proof state:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
H : LSeries f = LSeries g
n : ℕ
hn : n ≠ 0
⊢ f n = g n

Tactic:
refine eq_of_LSeries_eventually_eq hf hg ?_ hn

Result:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
H : LSeries f = LSeries g
n : ℕ
hn : n ≠ 0
⊢ (fun x => LSeries f ↑x) =ᶠ[Filter.atTop] fun x => LSeries g ↑x

Proof state:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
H : LSeries f = LSeries g
n : ℕ
hn : n ≠ 0
⊢ (fun x => LSeries f ↑x) =ᶠ[Filter.atTop] fun x => LSeries g ↑x

Tactic:
exact Filter.Eventually.of_forall fun x ↦ congr_fun H x

Result:
no goals