harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zip_eq_zip_take_min (l₁ : Array α) (l₂ : Array β) :
    zip l₁ l₂ = zip (l₁.take (min l₁.size l₂.size)) (l₂.take (min l₁.size l₂.size))

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
toList✝¹ : List α
toList✝ : List β
⊢ { toList := toList✝¹ }.zip { toList := toList✝ } =
    ({ toList := toList✝¹ }.take (min { toList := toList✝¹ }.size { toList := toList✝ }.size)).zip
      ({ toList := toList✝ }.take (min { toList := toList✝¹ }.size { toList := toList✝ }.size))

Tactic:
simp only [List.zip_toArray, size_toArray, List.take_toArray, mk.injEq]

Result:
case mk.mk
α : Type u_1
β : Type u_2
toList✝¹ : List α
toList✝ : List β
⊢ toList✝¹.zip toList✝ =
    (List.take (min toList✝¹.length toList✝.length) toList✝¹).zip
      (List.take (min toList✝¹.length toList✝.length) toList✝)

Proof state:
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Array β
⊢ l₁.zip l₂ = (l₁.take (min l₁.size l₂.size)).zip (l₂.take (min l₁.size l₂.size))

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
l₂ : Array β
toList✝ : List α
⊢ { toList := toList✝ }.zip l₂ =
    ({ toList := toList✝ }.take (min { toList := toList✝ }.size l₂.size)).zip
      (l₂.take (min { toList := toList✝ }.size l₂.size))

Proof state:
case mk
α : Type u_1
β : Type u_2
l₂ : Array β
toList✝ : List α
⊢ { toList := toList✝ }.zip l₂ =
    ({ toList := toList✝ }.take (min { toList := toList✝ }.size l₂.size)).zip
      (l₂.take (min { toList := toList✝ }.size l₂.size))

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
toList✝¹ : List α
toList✝ : List β
⊢ { toList := toList✝¹ }.zip { toList := toList✝ } =
    ({ toList := toList✝¹ }.take (min { toList := toList✝¹ }.size { toList := toList✝ }.size)).zip
      ({ toList := toList✝ }.take (min { toList := toList✝¹ }.size { toList := toList✝ }.size))

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
toList✝¹ : List α
toList✝ : List β
⊢ toList✝¹.zip toList✝ =
    (List.take (min toList✝¹.length toList✝.length) toList✝¹).zip
      (List.take (min toList✝¹.length toList✝.length) toList✝)

Tactic:
rw [List.zip_eq_zip_take_min]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem norm_kahler (x y : E) : ‖o.kahler x y‖ = ‖x‖ * ‖y‖

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ‖(o.kahler x) y‖ = ‖x‖ * ‖y‖

Tactic:
rw [← sq_eq_sq₀, Complex.sq_norm]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ Complex.normSq ((o.kahler x) y) = (‖x‖ * ‖y‖) ^ 2

case ha
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ 0 ≤ ‖(o.kahler x) y‖

case hb
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ 0 ≤ ‖x‖ * ‖y‖

Proof state:
case ha
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ 0 ≤ ‖(o.kahler x) y‖

Tactic:
positivity

Result:
no goals

Proof state:
case hb
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ 0 ≤ ‖x‖ * ‖y‖

Tactic:
positivity

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ Complex.normSq ((o.kahler x) y) = (‖x‖ * ‖y‖) ^ 2

Tactic:
linear_combination o.normSq_kahler x y

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem slt_eq_ult_of_msb_eq {x y : BitVec w} (h : x.msb = y.msb) :
    x.slt y = x.ult y

Proof state:
w : Nat
x y : BitVec w
h : x.msb = y.msb
⊢ ((if y.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat) < if y.msb = true then ↑y.toNat - ↑(2 ^ w) else ↑y.toNat) ↔
    x.toNat < y.toNat

Tactic:
cases y.msb <;> simp

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
h : x.msb = y.msb
⊢ x.slt y = x.ult y

Tactic:
simp only [BitVec.slt, toInt_eq_msb_cond, BitVec.ult, decide_eq_decide, h]

Result:
w : Nat
x y : BitVec w
h : x.msb = y.msb
⊢ ((if y.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat) < if y.msb = true then ↑y.toNat - ↑(2 ^ w) else ↑y.toNat) ↔
    x.toNat < y.toNat
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem Complex.isometryOfOrthonormal_symm_apply (v : OrthonormalBasis (Fin 2) ℝ F) (f : F) :
    (Complex.isometryOfOrthonormal v).symm f =
      (v.toBasis.coord 0 f : ℂ) + (v.toBasis.coord 1 f : ℂ) * I

Proof state:
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v : OrthonormalBasis (Fin 2) ℝ F
f : F
⊢ (isometryOfOrthonormal v).symm f = ↑((v.toBasis.coord 0) f) + ↑((v.toBasis.coord 1) f) * I

Tactic:
simp [Complex.isometryOfOrthonormal]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem UniformContinuous.iterate [UniformSpace β] (T : β → β) (n : ℕ) (h : UniformContinuous T) :
    UniformContinuous T^[n]

Proof state:
β : Type ub
inst✝ : UniformSpace β
T : β → β
n : ℕ
h : UniformContinuous T
⊢ UniformContinuous T^[n]

Tactic:
induction n with
| zero => exact uniformContinuous_id
| succ n hn => exact Function.iterate_succ _ _ ▸ UniformContinuous.comp hn h

Result:
no goals

Proof state:
case zero
β : Type ub
inst✝ : UniformSpace β
T : β → β
h : UniformContinuous T
⊢ UniformContinuous T^[0]

Tactic:
exact uniformContinuous_id

Result:
no goals

Proof state:
case succ
β : Type ub
inst✝ : UniformSpace β
T : β → β
h : UniformContinuous T
n : ℕ
hn : UniformContinuous T^[n]
⊢ UniformContinuous T^[n + 1]

Tactic:
exact Function.iterate_succ _ _ ▸ UniformContinuous.comp hn h

Result:
no goals
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem comap_const (f : R →+* S) (U : Opens (PrimeSpectrum.Top R))
    (V : Opens (PrimeSpectrum.Top S)) (hUV : V.1 ⊆ PrimeSpectrum.comap f ⁻¹' U.1) (a b : R)
    (hb : ∀ x : PrimeSpectrum R, x ∈ U → b ∈ x.asIdeal.primeCompl) :
    comap f U V hUV (const R a b U hb) =
      const S (f a) (f b) V fun p hpV => hb (PrimeSpectrum.comap f p) (hUV hpV) :=
  Subtype.eq <|
    funext fun p => by
      rw [comap_apply, const_apply, const_apply, Localization.localRingHom_mk']

Proof state:
R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier
a b : R
hb : ∀ x ∈ U, b ∈ x.asIdeal.primeCompl
p : ↥(unop (op V))
⊢ ↑((comap f U V hUV) (const R a b U hb)) p = ↑(const S (f a) (f b) V ⋯) p

Tactic:
rw [comap_apply, const_apply, const_apply, Localization.localRingHom_mk']

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem lt_omega0_opow {a b : Ordinal} (hb : b ≠ 0) :
    a < ω ^ b ↔ ∃ c < b, ∃ n : ℕ, a < ω ^ c * n

Proof state:
case h
a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
n : ℕ
hn : a / ω ^ log ω a = ↑n
⊢ a < ω ^ log ω a * succ (a / ω ^ log ω a)

Tactic:
exact lt_mul_succ_div a (opow_ne_zero _ omega0_ne_zero)

Result:
no goals

Proof state:
a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
⊢ ∃ n, a < ω ^ log ω a * ↑n

Tactic:
obtain ⟨n, hn⟩ := lt_omega0.1 (div_opow_log_lt a one_lt_omega0)

Result:
case intro
a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
n : ℕ
hn : a / ω ^ log ω a = ↑n
⊢ ∃ n, a < ω ^ log ω a * ↑n

Proof state:
case intro
a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
n : ℕ
hn : a / ω ^ log ω a = ↑n
⊢ ∃ n, a < ω ^ log ω a * ↑n

Tactic:
use n.succ

Result:
case h
a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
n : ℕ
hn : a / ω ^ log ω a = ↑n
⊢ a < ω ^ log ω a * ↑n.succ

Proof state:
case h
a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
n : ℕ
hn : a / ω ^ log ω a = ↑n
⊢ a < ω ^ log ω a * ↑n.succ

Tactic:
rw [natCast_succ, ← hn]

Result:
case h
a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
n : ℕ
hn : a / ω ^ log ω a = ↑n
⊢ a < ω ^ log ω a * succ (a / ω ^ log ω a)

Proof state:
a b : Ordinal.{u_1}
hb : b ≠ 0
⊢ a < ω ^ b ↔ ∃ c < b, ∃ n, a < ω ^ c * ↑n

Tactic:
refine ⟨fun ha ↦ ⟨_, lt_log_of_lt_opow hb ha, ?_⟩,
  fun ⟨c, hc, n, hn⟩ ↦ hn.trans (omega0_opow_mul_nat_lt hc n)⟩

Result:
a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
⊢ ∃ n, a < ω ^ log ω a * ↑n
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem EqOnSource.symm' {e e' : PartialEquiv α β} (h : e ≈ e') : e.symm ≈ e'.symm

Proof state:
case refine_1
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
⊢ RightInvOn (↑e'.symm) (↑e) e'.target

Tactic:
exact e'.rightInvOn.congr_right e'.symm_mapsTo (source_eq h ▸ h.eqOn.symm)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
⊢ e.symm ≈ e'.symm

Tactic:
refine ⟨target_eq h, eqOn_of_leftInvOn_of_rightInvOn e.leftInvOn ?_ ?_⟩ <;>
  simp only [symm_source, target_eq h, source_eq h, e'.symm_mapsTo]

Result:
case refine_1
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
⊢ RightInvOn (↑e'.symm) (↑e) e'.target
-- Mathlib/Data/List/Sym.lean
theorem mk_mem_sym2_iff {xs : List α} {a b : α} :
    s(a, b) ∈ xs.sym2 ↔ a ∈ xs ∧ b ∈ xs

Proof state:
case mpr.intro
α : Type u_1
xs : List α
a b : α
ha : a ∈ xs
hb : b ∈ xs
⊢ s(a, b) ∈ xs.sym2

Tactic:
exact mk_mem_sym2 ha hb

Result:
no goals

Proof state:
case mp
α : Type u_1
xs : List α
a b : α
h : s(a, b) ∈ xs.sym2
⊢ a ∈ xs ∧ b ∈ xs

Tactic:
exact ⟨left_mem_of_mk_mem_sym2 h, right_mem_of_mk_mem_sym2 h⟩

Result:
no goals

Proof state:
α : Type u_1
xs : List α
a b : α
⊢ s(a, b) ∈ xs.sym2 ↔ a ∈ xs ∧ b ∈ xs

Tactic:
constructor

Result:
case mp
α : Type u_1
xs : List α
a b : α
⊢ s(a, b) ∈ xs.sym2 → a ∈ xs ∧ b ∈ xs

case mpr
α : Type u_1
xs : List α
a b : α
⊢ a ∈ xs ∧ b ∈ xs → s(a, b) ∈ xs.sym2

Proof state:
case mp
α : Type u_1
xs : List α
a b : α
⊢ s(a, b) ∈ xs.sym2 → a ∈ xs ∧ b ∈ xs

Tactic:
intro h

Result:
case mp
α : Type u_1
xs : List α
a b : α
h : s(a, b) ∈ xs.sym2
⊢ a ∈ xs ∧ b ∈ xs

Proof state:
case mpr
α : Type u_1
xs : List α
a b : α
⊢ a ∈ xs ∧ b ∈ xs → s(a, b) ∈ xs.sym2

Tactic:
rintro ⟨ha, hb⟩

Result:
case mpr.intro
α : Type u_1
xs : List α
a b : α
ha : a ∈ xs
hb : b ∈ xs
⊢ s(a, b) ∈ xs.sym2
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem mul_comm (a b : Rat) : a * b = b * a

Proof state:
a b : Rat
⊢ a * b = b * a

Tactic:
simp [mul_def, normalize_eq_mkRat, Int.mul_comm, Nat.mul_comm]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem exists_subset_or_subset_of_two_mul_lt_ncard {n : ℕ} (hst : 2 * n < (s ∪ t).ncard) :
    ∃ r : Set α, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)

Proof state:
α : Type u_1
s t : Set α
n : ℕ
hu : (s ∪ t).Finite
hst : 2 * n < (⋯.toFinset ∪ ⋯.toFinset).card
r' : Finset α
hnr' : n < r'.card
hr' : r' ⊆ ⋯.toFinset ∨ r' ⊆ ⋯.toFinset
⊢ n < (↑r').ncard

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
n : ℕ
hst : 2 * n < (s ∪ t).ncard
⊢ ∃ r, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)

Tactic:
classical
have hu := finite_of_ncard_ne_zero ((Nat.zero_le _).trans_lt hst).ne.symm
rw [ncard_eq_toFinset_card _ hu,
  Finite.toFinset_union (hu.subset subset_union_left)
    (hu.subset subset_union_right)] at hst
obtain ⟨r', hnr', hr'⟩ := Finset.exists_subset_or_subset_of_two_mul_lt_card hst
exact ⟨r', by simpa, by simpa using hr'⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
s t : Set α
n : ℕ
hu : (s ∪ t).Finite
hst : 2 * n < (⋯.toFinset ∪ ⋯.toFinset).card
r' : Finset α
hnr' : n < r'.card
hr' : r' ⊆ ⋯.toFinset ∨ r' ⊆ ⋯.toFinset
⊢ ∃ r, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)

Tactic:
exact ⟨r', by simpa, by simpa using hr'⟩

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
n : ℕ
hu : (s ∪ t).Finite
hst : 2 * n < (⋯.toFinset ∪ ⋯.toFinset).card
r' : Finset α
hnr' : n < r'.card
hr' : r' ⊆ ⋯.toFinset ∨ r' ⊆ ⋯.toFinset
⊢ ↑r' ⊆ s ∨ ↑r' ⊆ t

Tactic:
simpa using hr'

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
n : ℕ
hst : 2 * n < (s ∪ t).ncard
⊢ ∃ r, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)

Tactic:
have hu := finite_of_ncard_ne_zero ((Nat.zero_le _).trans_lt hst).ne.symm

Result:
α : Type u_1
s t : Set α
n : ℕ
hst : 2 * n < (s ∪ t).ncard
hu : (s ∪ t).Finite
⊢ ∃ r, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)

Proof state:
α : Type u_1
s t : Set α
n : ℕ
hst : 2 * n < (s ∪ t).ncard
hu : (s ∪ t).Finite
⊢ ∃ r, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)

Tactic:
rw [ncard_eq_toFinset_card _ hu,
  Finite.toFinset_union (hu.subset subset_union_left)
    (hu.subset subset_union_right)] at hst

Result:
α : Type u_1
s t : Set α
n : ℕ
hu : (s ∪ t).Finite
hst : 2 * n < (⋯.toFinset ∪ ⋯.toFinset).card
⊢ ∃ r, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)

Proof state:
α : Type u_1
s t : Set α
n : ℕ
hu : (s ∪ t).Finite
hst : 2 * n < (⋯.toFinset ∪ ⋯.toFinset).card
⊢ ∃ r, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)

Tactic:
obtain ⟨r', hnr', hr'⟩ := Finset.exists_subset_or_subset_of_two_mul_lt_card hst

Result:
case intro.intro
α : Type u_1
s t : Set α
n : ℕ
hu : (s ∪ t).Finite
hst : 2 * n < (⋯.toFinset ∪ ⋯.toFinset).card
r' : Finset α
hnr' : n < r'.card
hr' : r' ⊆ ⋯.toFinset ∨ r' ⊆ ⋯.toFinset
⊢ ∃ r, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
-- Mathlib/GroupTheory/Nilpotent.lean
theorem isNilpotent_pi_of_bounded_class [∀ i, IsNilpotent (Gs i)] (n : ℕ)
    (h : ∀ i, Group.nilpotencyClass (Gs i) ≤ n) : IsNilpotent (∀ i, Gs i)

Proof state:
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ (pi Set.univ fun i => lowerCentralSeries (Gs i) n) ≤ ⊥

Tactic:
rw [← eq_bot_iff, pi_eq_bot_iff]

Result:
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ ∀ (i : η), lowerCentralSeries (Gs i) n = ⊥

Proof state:
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ lowerCentralSeries ((i : η) → Gs i) n ≤ ⊥

Tactic:
apply le_trans (lowerCentralSeries_pi_le _)

Result:
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ (pi Set.univ fun i => lowerCentralSeries (Gs i) n) ≤ ⊥

Proof state:
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ ∃ n, lowerCentralSeries ((i : η) → Gs i) n = ⊥

Tactic:
refine ⟨n, ?_⟩

Result:
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ lowerCentralSeries ((i : η) → Gs i) n = ⊥

Proof state:
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ ∀ (i : η), lowerCentralSeries (Gs i) n = ⊥

Tactic:
intro i

Result:
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
i : η
⊢ lowerCentralSeries (Gs i) n = ⊥

Proof state:
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ lowerCentralSeries ((i : η) → Gs i) n = ⊥

Tactic:
rw [eq_bot_iff]

Result:
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ lowerCentralSeries ((i : η) → Gs i) n ≤ ⊥

Proof state:
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ IsNilpotent ((i : η) → Gs i)

Tactic:
rw [nilpotent_iff_lowerCentralSeries]

Result:
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ ∃ n, lowerCentralSeries ((i : η) → Gs i) n = ⊥

Proof state:
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
i : η
⊢ lowerCentralSeries (Gs i) n = ⊥

Tactic:
apply lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr (h i)

Result:
no goals
-- Mathlib/Order/GameAdd.lean
theorem gameAdd_iff : ∀ {x y : α × α},
    GameAdd rα (Sym2.mk x) (Sym2.mk y) ↔ Prod.GameAdd rα rα x y ∨ Prod.GameAdd rα rα x.swap y

Proof state:
α : Type u_1
rα : α → α → Prop
⊢ ∀ {x y : α × α}, GameAdd rα (Sym2.mk x) (Sym2.mk y) ↔ Prod.GameAdd rα rα x y ∨ Prod.GameAdd rα rα x.swap y

Tactic:
rintro ⟨_, _⟩ ⟨_, _⟩

Result:
case mk.mk
α : Type u_1
rα : α → α → Prop
fst✝¹ snd✝¹ fst✝ snd✝ : α
⊢ GameAdd rα s(fst✝¹, snd✝¹) s(fst✝, snd✝) ↔
    Prod.GameAdd rα rα (fst✝¹, snd✝¹) (fst✝, snd✝) ∨ Prod.GameAdd rα rα (fst✝¹, snd✝¹).swap (fst✝, snd✝)

Proof state:
case mk.mk
α : Type u_1
rα : α → α → Prop
fst✝¹ snd✝¹ fst✝ snd✝ : α
⊢ GameAdd rα s(fst✝¹, snd✝¹) s(fst✝, snd✝) ↔
    Prod.GameAdd rα rα (fst✝¹, snd✝¹) (fst✝, snd✝) ∨ Prod.GameAdd rα rα (fst✝¹, snd✝¹).swap (fst✝, snd✝)

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
lemma farFromTriangleFree [ExplicitDisjoint t] {ε : 𝕜}
    (ht : ε * ((Fintype.card α + Fintype.card β + Fintype.card γ) ^ 2 : ℕ) ≤ #t) :
    (graph t).FarFromTriangleFree ε :=
  farFromTriangleFree_of_disjoint_triangles (t.map toTriangle)
    (map_subset_iff_subset_preimage.2 fun x hx ↦ by simpa using toTriangle_is3Clique hx)
    (map_toTriangle_disjoint t) <| by simpa [add_assoc] using ht

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝⁷ : LinearOrderedField 𝕜
t : Finset (α × β × γ)
inst✝⁶ : DecidableEq α
inst✝⁵ : DecidableEq β
inst✝⁴ : DecidableEq γ
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype γ
inst✝ : ExplicitDisjoint t
ε : 𝕜
ht : ε * ↑((Fintype.card α + Fintype.card β + Fintype.card γ) ^ 2) ≤ ↑(#t)
x : α × β × γ
hx : x ∈ t
⊢ x ∈ ((graph t).cliqueFinset 3).preimage ⇑toTriangle ⋯

Tactic:
simpa using toTriangle_is3Clique hx

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝⁷ : LinearOrderedField 𝕜
t : Finset (α × β × γ)
inst✝⁶ : DecidableEq α
inst✝⁵ : DecidableEq β
inst✝⁴ : DecidableEq γ
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype γ
inst✝ : ExplicitDisjoint t
ε : 𝕜
ht : ε * ↑((Fintype.card α + Fintype.card β + Fintype.card γ) ^ 2) ≤ ↑(#t)
⊢ ε * ↑(Fintype.card (α ⊕ β ⊕ γ) ^ 2) ≤ ↑(#(map toTriangle t))

Tactic:
simpa [add_assoc] using ht

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/MulOppositeLemmas.lean
theorem normal_unop {H : Subgroup Gᵐᵒᵖ} : H.unop.Normal ↔ H.Normal

Proof state:
G : Type u_2
inst✝ : Group G
H : Subgroup Gᵐᵒᵖ
⊢ H.unop.Normal ↔ H.Normal

Tactic:
rw [← normal_op, op_unop]

Result:
no goals
-- Mathlib/LinearAlgebra/CrossProduct.lean
theorem cross_dot_cross (u v w x : Fin 3 → R) :
    u ×₃ v ⬝ᵥ w ×₃ x = u ⬝ᵥ w * v ⬝ᵥ x - u ⬝ᵥ x * v ⬝ᵥ w

Proof state:
R : Type u_1
inst✝ : CommRing R
u v w x : Fin 3 → R
⊢ ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 0 *
          ![w 1 * x 2 - w 2 * x 1, w 2 * x 0 - w 0 * x 2, w 0 * x 1 - w 1 * x 0] 0 +
        ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 1 *
          ![w 1 * x 2 - w 2 * x 1, w 2 * x 0 - w 0 * x 2, w 0 * x 1 - w 1 * x 0] 1 +
      ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 2 *
        ![w 1 * x 2 - w 2 * x 1, w 2 * x 0 - w 0 * x 2, w 0 * x 1 - w 1 * x 0] 2 =
    (u 0 * w 0 + u 1 * w 1 + u 2 * w 2) * (v 0 * x 0 + v 1 * x 1 + v 2 * x 2) -
      (u 0 * x 0 + u 1 * x 1 + u 2 * x 2) * (v 0 * w 0 + v 1 * w 1 + v 2 * w 2)

Tactic:
norm_num

Result:
R : Type u_1
inst✝ : CommRing R
u v w x : Fin 3 → R
⊢ (u 1 * v 2 - u 2 * v 1) * (w 1 * x 2 - w 2 * x 1) + (u 2 * v 0 - u 0 * v 2) * (w 2 * x 0 - w 0 * x 2) +
      (u 0 * v 1 - u 1 * v 0) * (w 0 * x 1 - w 1 * x 0) =
    (u 0 * w 0 + u 1 * w 1 + u 2 * w 2) * (v 0 * x 0 + v 1 * x 1 + v 2 * x 2) -
      (u 0 * x 0 + u 1 * x 1 + u 2 * x 2) * (v 0 * w 0 + v 1 * w 1 + v 2 * w 2)

Proof state:
R : Type u_1
inst✝ : CommRing R
u v w x : Fin 3 → R
⊢ (crossProduct u) v ⬝ᵥ (crossProduct w) x = u ⬝ᵥ w * v ⬝ᵥ x - u ⬝ᵥ x * v ⬝ᵥ w

Tactic:
simp_rw [cross_apply, vec3_dotProduct]

Result:
R : Type u_1
inst✝ : CommRing R
u v w x : Fin 3 → R
⊢ ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 0 *
          ![w 1 * x 2 - w 2 * x 1, w 2 * x 0 - w 0 * x 2, w 0 * x 1 - w 1 * x 0] 0 +
        ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 1 *
          ![w 1 * x 2 - w 2 * x 1, w 2 * x 0 - w 0 * x 2, w 0 * x 1 - w 1 * x 0] 1 +
      ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 2 *
        ![w 1 * x 2 - w 2 * x 1, w 2 * x 0 - w 0 * x 2, w 0 * x 1 - w 1 * x 0] 2 =
    (u 0 * w 0 + u 1 * w 1 + u 2 * w 2) * (v 0 * x 0 + v 1 * x 1 + v 2 * x 2) -
      (u 0 * x 0 + u 1 * x 1 + u 2 * x 2) * (v 0 * w 0 + v 1 * w 1 + v 2 * w 2)

Proof state:
R : Type u_1
inst✝ : CommRing R
u v w x : Fin 3 → R
⊢ (u 1 * v 2 - u 2 * v 1) * (w 1 * x 2 - w 2 * x 1) + (u 2 * v 0 - u 0 * v 2) * (w 2 * x 0 - w 0 * x 2) +
      (u 0 * v 1 - u 1 * v 0) * (w 0 * x 1 - w 1 * x 0) =
    (u 0 * w 0 + u 1 * w 1 + u 2 * w 2) * (v 0 * x 0 + v 1 * x 1 + v 2 * x 2) -
      (u 0 * x 0 + u 1 * x 1 + u 2 * x 2) * (v 0 * w 0 + v 1 * w 1 + v 2 * w 2)

Tactic:
ring

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem eq_ones_iff {c : Composition n} : c = ones n ↔ ∀ i ∈ c.blocks, i = 1

Proof state:
n : ℕ
c : Composition n
⊢ c = ones n ↔ ∀ i ∈ c.blocks, i = 1

Tactic:
constructor

Result:
case mp
n : ℕ
c : Composition n
⊢ c = ones n → ∀ i ∈ c.blocks, i = 1

case mpr
n : ℕ
c : Composition n
⊢ (∀ i ∈ c.blocks, i = 1) → c = ones n

Proof state:
case mpr.blocks
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
this : c.blocks.length = n
⊢ c.blocks = (ones n).blocks

Tactic:
rw [A, this, ones_blocks]

Result:
no goals

Proof state:
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
⊢ c.blocks.length = n

Tactic:
conv_rhs => rw [← c.blocks_sum, A]

Result:
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
⊢ c.blocks.length = (replicate c.blocks.length 1).sum

Proof state:
case mpr
n : ℕ
c : Composition n
⊢ (∀ i ∈ c.blocks, i = 1) → c = ones n

Tactic:
intro H

Result:
case mpr
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
⊢ c = ones n

Proof state:
case mp
n : ℕ
⊢ ∀ i ∈ (ones n).blocks, i = 1

Tactic:
exact fun i => eq_of_mem_replicate

Result:
no goals

Proof state:
case mp
n : ℕ
c : Composition n
⊢ c = ones n → ∀ i ∈ c.blocks, i = 1

Tactic:
rintro rfl

Result:
case mp
n : ℕ
⊢ ∀ i ∈ (ones n).blocks, i = 1

Proof state:
case mpr
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
⊢ c = ones n

Tactic:
ext1

Result:
case mpr.blocks
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
⊢ c.blocks = (ones n).blocks

Proof state:
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
⊢ c.blocks.length = (replicate c.blocks.length 1).sum

Tactic:
simp

Result:
no goals

Proof state:
case mpr.blocks
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
⊢ c.blocks = (ones n).blocks

Tactic:
have A : c.blocks = replicate c.blocks.length 1 := eq_replicate_of_mem H

Result:
case mpr.blocks
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
⊢ c.blocks = (ones n).blocks

Proof state:
case mpr.blocks
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
⊢ c.blocks = (ones n).blocks

Tactic:
have : c.blocks.length = n := by
  conv_rhs => rw [← c.blocks_sum, A]
  simp

Result:
case mpr.blocks
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
this : c.blocks.length = n
⊢ c.blocks = (ones n).blocks