harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_push {a : Array α} {x} : (a.push x)[i]? = if i = a.size then some x else a[i]?

Proof state:
case isFalse.isFalse
α : Type u_1
i : Nat
a : Array α
x : α
h✝¹ : ¬i < a.size + 1
h✝ : ¬i = a.size
⊢ none = if h : i < a.size then some a[i] else none

Tactic:
split

Result:
case isFalse.isFalse.isTrue
α : Type u_1
i : Nat
a : Array α
x : α
h✝² : ¬i < a.size + 1
h✝¹ : ¬i = a.size
h✝ : i < a.size
⊢ none = some a[i]

case isFalse.isFalse.isFalse
α : Type u_1
i : Nat
a : Array α
x : α
h✝² : ¬i < a.size + 1
h✝¹ : ¬i = a.size
h✝ : ¬i < a.size
⊢ none = none

Proof state:
case isFalse.isFalse.isTrue
α : Type u_1
i : Nat
a : Array α
x : α
h✝² : ¬i < a.size + 1
h✝¹ : ¬i = a.size
h✝ : i < a.size
⊢ none = some a[i]

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
i : Nat
a : Array α
x : α
⊢ (a.push x)[i]? = if i = a.size then some x else a[i]?

Tactic:
simp [getElem?_def, getElem_push]

Result:
α : Type u_1
i : Nat
a : Array α
x : α
⊢ (if i < a.size + 1 then some (if h : i < a.size then a[i] else x) else none) =
    if i = a.size then some x else if h : i < a.size then some a[i] else none

Proof state:
α : Type u_1
i : Nat
a : Array α
x : α
⊢ (if i < a.size + 1 then some (if h : i < a.size then a[i] else x) else none) =
    if i = a.size then some x else if h : i < a.size then some a[i] else none

Tactic:
(repeat' split) <;> first | rfl | omega

Result:
no goals

Proof state:
α : Type u_1
i : Nat
a : Array α
x : α
⊢ (if i < a.size + 1 then some (if h : i < a.size then a[i] else x) else none) =
    if i = a.size then some x else if h : i < a.size then some a[i] else none

Tactic:
repeat' split

Result:
case isTrue.isTrue.isTrue
α : Type u_1
i : Nat
a : Array α
x : α
h✝² : i < a.size + 1
h✝¹ : i < a.size
h✝ : i = a.size
⊢ some a[i] = some x

case isTrue.isTrue.isFalse
α : Type u_1
i : Nat
a : Array α
x : α
h✝² : i < a.size + 1
h✝¹ : i < a.size
h✝ : ¬i = a.size
⊢ some a[i] = some a[i]

case isTrue.isFalse.isTrue
α : Type u_1
i : Nat
a : Array α
x : α
h✝² : i < a.size + 1
h✝¹ : ¬i < a.size
h✝ : i = a.size
⊢ some x = some x

case isTrue.isFalse.isFalse
α : Type u_1
i : Nat
a : Array α
x : α
h✝² : i < a.size + 1
h✝¹ : ¬i < a.size
h✝ : ¬i = a.size
⊢ some x = none

case isFalse.isTrue
α : Type u_1
i : Nat
a : Array α
x : α
h✝¹ : ¬i < a.size + 1
h✝ : i = a.size
⊢ none = some x

case isFalse.isFalse.isTrue
α : Type u_1
i : Nat
a : Array α
x : α
h✝² : ¬i < a.size + 1
h✝¹ : ¬i = a.size
h✝ : i < a.size
⊢ none = some a[i]

case isFalse.isFalse.isFalse
α : Type u_1
i : Nat
a : Array α
x : α
h✝² : ¬i < a.size + 1
h✝¹ : ¬i = a.size
h✝ : ¬i < a.size
⊢ none = none

Proof state:
case isFalse.isFalse.isFalse
α : Type u_1
i : Nat
a : Array α
x : α
h✝² : ¬i < a.size + 1
h✝¹ : ¬i = a.size
h✝ : ¬i < a.size
⊢ none = none

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/PiTopology.lean
theorem tendsto_pow_zero_of_constantCoeff_nilpotent [CommSemiring R]
    {f} (hf : IsNilpotent (constantCoeff σ R f)) :
    Tendsto (fun n : ℕ => f ^ n) atTop (nhds 0)

Proof state:
case intro
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hm : (constantCoeff σ R) f ^ m = 0
⊢ Tendsto (fun n => f ^ n) atTop (nhds 0)

Tactic:
simp_rw [tendsto_iff_coeff_tendsto, coeff_zero]

Result:
case intro
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hm : (constantCoeff σ R) f ^ m = 0
⊢ ∀ (d : σ →₀ ℕ), Tendsto (fun i => (coeff R d) (f ^ i)) atTop (nhds 0)

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
hf : IsNilpotent ((constantCoeff σ R) f)
⊢ Tendsto (fun n => f ^ n) atTop (nhds 0)

Tactic:
obtain ⟨m, hm⟩ := hf

Result:
case intro
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hm : (constantCoeff σ R) f ^ m = 0
⊢ Tendsto (fun n => f ^ n) atTop (nhds 0)

Proof state:
case intro
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hm : (constantCoeff σ R) f ^ m = 0
⊢ ∀ (d : σ →₀ ℕ), Tendsto (fun i => (coeff R d) (f ^ i)) atTop (nhds 0)

Tactic:
exact fun d ↦ tendsto_atTop_of_eventually_const fun n hn ↦
  coeff_eq_zero_of_constantCoeff_nilpotent hm hn

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
hf : IsNilpotent ((constantCoeff σ R) f)
⊢ Tendsto (fun n => f ^ n) atTop (nhds 0)

Tactic:
classical
obtain ⟨m, hm⟩ := hf
simp_rw [tendsto_iff_coeff_tendsto, coeff_zero]
exact fun d ↦ tendsto_atTop_of_eventually_const fun n hn ↦
  coeff_eq_zero_of_constantCoeff_nilpotent hm hn

Result:
no goals
-- Mathlib/Algebra/Order/Field/Defs.lean
/-- Equality holds when `c ≠ 0`. See `mul_div_mul_left`. -/
lemma le_mul_div_mul_left (h : a / b ≤ 0) : a / b ≤ c * a / (c * b)

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b : α
h : a / b ≤ 0
⊢ a / b ≤ 0 * a / (0 * b)

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c : α
h : a / b ≤ 0
⊢ a / b ≤ c * a / (c * b)

Tactic:
obtain rfl | hc := eq_or_ne c 0

Result:
case inl
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b : α
h : a / b ≤ 0
⊢ a / b ≤ 0 * a / (0 * b)

case inr
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c : α
h : a / b ≤ 0
hc : c ≠ 0
⊢ a / b ≤ c * a / (c * b)

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c : α
h : a / b ≤ 0
hc : c ≠ 0
⊢ a / b ≤ c * a / (c * b)

Tactic:
rw [mul_div_mul_left _ _ hc]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Bisect.lean
theorem le_avg_right (h : b ≤ a) : b ≤ avg a b

Proof state:
b a : Nat
h : b ≤ a
⊢ b * 2 ≤ a + b

Tactic:
simp_arith [*]

Result:
no goals

Proof state:
b a : Nat
h : b ≤ a
⊢ b ≤ a.avg b

Tactic:
apply (Nat.le_div_iff_mul_le Nat.zero_lt_two).mpr

Result:
b a : Nat
h : b ≤ a
⊢ b * 2 ≤ a + b
-- Mathlib/Data/Finset/NAry.lean
theorem mem_image₂ : c ∈ image₂ f s t ↔ ∃ a ∈ s, ∃ b ∈ t, f a b = c

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
c : γ
⊢ c ∈ image₂ f s t ↔ ∃ a ∈ s, ∃ b ∈ t, f a b = c

Tactic:
simp [image₂, and_assoc]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendsto_prod_filter_iff {c : β} :
    Tendsto (↿F) (p ×ˢ p') (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun _ => c) p p'

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
c : β
⊢ Tendsto (↿F) (p ×ˢ p') (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun x => c) p p'

Tactic:
simp_rw [nhds_eq_comap_uniformity, tendsto_comap_iff]

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
c : β
⊢ Tendsto (Prod.mk c ∘ ↿F) (p ×ˢ p') (𝓤 β) ↔ TendstoUniformlyOnFilter F (fun x => c) p p'

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
c : β
⊢ Tendsto (Prod.mk c ∘ ↿F) (p ×ˢ p') (𝓤 β) ↔ TendstoUniformlyOnFilter F (fun x => c) p p'

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem coprime_sq_sub_mul_of_odd_even {m n : ℤ} (h : Int.gcd m n = 1) (hm : m % 2 = 1)
    (hn : n % 2 = 0) : Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1

Proof state:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ 2 * m * n = 2 * n * m

Tactic:
ring

Result:
no goals

Proof state:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (-(m ^ 2 - n ^ 2)).natAbs.gcd (2 * m * n).natAbs = 1

Tactic:
rw [(by ring : 2 * m * n = 2 * n * m), (by ring : -(m ^ 2 - n ^ 2) = n ^ 2 - m ^ 2)]

Result:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (n ^ 2 - m ^ 2).natAbs.gcd (2 * n * m).natAbs = 1

Proof state:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ -(m ^ 2 - n ^ 2) = n ^ 2 - m ^ 2

Tactic:
ring

Result:
no goals

Proof state:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1

Tactic:
rw [Int.gcd, ← Int.natAbs_neg (m ^ 2 - n ^ 2)]

Result:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (-(m ^ 2 - n ^ 2)).natAbs.gcd (2 * m * n).natAbs = 1

Proof state:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ n.gcd m = 1

Tactic:
rwa [Int.gcd_comm]

Result:
no goals

Proof state:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (n ^ 2 - m ^ 2).natAbs.gcd (2 * n * m).natAbs = 1

Tactic:
apply coprime_sq_sub_mul_of_even_odd _ hn hm

Result:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ n.gcd m = 1
-- Mathlib/RingTheory/NoetherNormalization.lean
theorem exists_integral_inj_algHom_of_quotient (I : Ideal (MvPolynomial (Fin n) k))
    (hi : I ≠ ⊤) : ∃ s ≤ n, ∃ g : (MvPolynomial (Fin s) k) →ₐ[k] ((MvPolynomial (Fin n) k) ⧸ I),
    Function.Injective g ∧ g.IsIntegral

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
I : Ideal (MvPolynomial (Fin 0) k)
hi : I ≠ ⊤
a b : MvPolynomial (Fin 0) k
hab : a - b ∈ I
neq : ¬a = b
eq : a - b = MvPolynomial.C (MvPolynomial.coeff 0 (a - b))
ne : MvPolynomial.coeff 0 (a - b) ≠ 0
c : k
left✝ : MvPolynomial.coeff 0 (a - b) * c = 1
eqr : c * MvPolynomial.coeff 0 (a - b) = 1
⊢ c • (a - b) = 1

Tactic:
rw [MvPolynomial.smul_eq_C_mul, eq, ← RingHom.map_mul, eqr, MvPolynomial.C_1]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma ext_spanning {M M' : Matroid α} (h : M.E = M'.E)
    (hsp : ∀ S, S ⊆ M.E → (M.Spanning S ↔ M'.Spanning S )) : M = M'

Proof state:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
⊢ M = M'

Tactic:
rw [← dual_inj, ext_iff_indep, dual_ground, dual_ground, and_iff_right h]

Result:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
⊢ ∀ ⦃I : Set α⦄, I ⊆ M.E → (M✶.Indep I ↔ M'✶.Indep I)

Proof state:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
S : Set α
hSE : S ⊆ M.E
⊢ M.Spanning S ↔ M'.Spanning S

Tactic:
rw [hsp _ hSE]

Result:
no goals

Proof state:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
I : Set α
hIE : I ⊆ M.E
⊢ M✶.Indep I ↔ M'✶.Indep I

Tactic:
rw [← coindep_def, ← coindep_def, coindep_iff_compl_spanning, coindep_iff_compl_spanning, hsp', h]

Result:
no goals

Proof state:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
⊢ M = M'

Tactic:
have hsp' : M.Spanning = M'.Spanning := by
  ext S
  refine (em (S ⊆ M.E)).elim (fun hSE ↦ by rw [hsp _ hSE] )
    (fun hSE ↦ iff_of_false (fun h ↦ hSE h.subset_ground)
    (fun h' ↦ hSE (h'.subset_ground.trans h.symm.subset)))

Result:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
⊢ M = M'

Proof state:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
⊢ ∀ ⦃I : Set α⦄, I ⊆ M.E → (M✶.Indep I ↔ M'✶.Indep I)

Tactic:
intro I hIE

Result:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
I : Set α
hIE : I ⊆ M.E
⊢ M✶.Indep I ↔ M'✶.Indep I

Proof state:
case h.a
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
S : Set α
⊢ M.Spanning S ↔ M'.Spanning S

Tactic:
refine (em (S ⊆ M.E)).elim (fun hSE ↦ by rw [hsp _ hSE] )
  (fun hSE ↦ iff_of_false (fun h ↦ hSE h.subset_ground)
  (fun h' ↦ hSE (h'.subset_ground.trans h.symm.subset)))

Result:
no goals

Proof state:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
⊢ M.Spanning = M'.Spanning

Tactic:
ext S

Result:
case h.a
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
S : Set α
⊢ M.Spanning S ↔ M'.Spanning S
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem Filter.HasBasis.cauchySeq_iff {γ} [Nonempty β] [SemilatticeSup β] {u : β → α} {p : γ → Prop}
    {s : γ → Set (α × α)} (h : (𝓤 α).HasBasis p s) :
    CauchySeq u ↔ ∀ i, p i → ∃ N, ∀ m, N ≤ m → ∀ n, N ≤ n → (u m, u n) ∈ s i

Proof state:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
h : (𝓤 α).HasBasis p s
⊢ Tendsto (Prod.map u u) (atTop ×ˢ atTop) (𝓤 α) ↔
    ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i

Tactic:
refine (atTop_basis.prod_self.tendsto_iff h).trans ?_

Result:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
h : (𝓤 α).HasBasis p s
⊢ (∀ (ib : γ), p ib → ∃ ia, True ∧ ∀ x ∈ Ici ia ×ˢ Ici ia, Prod.map u u x ∈ s ib) ↔
    ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i

Proof state:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
h : (𝓤 α).HasBasis p s
⊢ CauchySeq u ↔ ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i

Tactic:
rw [cauchySeq_iff_tendsto, ← prod_atTop_atTop_eq]

Result:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
h : (𝓤 α).HasBasis p s
⊢ Tendsto (Prod.map u u) (atTop ×ˢ atTop) (𝓤 α) ↔
    ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i

Proof state:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → Set (α × α)
h : (𝓤 α).HasBasis p s
⊢ (∀ (ib : γ), p ib → ∃ ia, True ∧ ∀ x ∈ Ici ia ×ˢ Ici ia, Prod.map u u x ∈ s ib) ↔
    ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i

Tactic:
simp only [exists_prop, true_and, MapsTo, preimage, subset_def, Prod.forall, mem_prod_eq,
  mem_setOf_eq, mem_Ici, and_imp, Prod.map, @forall_swap (_ ≤ _) β]

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts/FunctorCategory.lean
@[simp]
lemma associator_hom_app (F₁ F₂ F₃ : J ⥤ C) (j : J) :
    (α_ F₁ F₂ F₃).hom.app j = (α_ _ _ _).hom

Proof state:
case h_snd.h_fst
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ ((α_ F₁ F₂ F₃).hom.app j ≫ (snd F₁ (F₂ ⊗ F₃)).app j) ≫ (fst F₂ F₃).app j =
    ((α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j)) ≫ fst (F₂.obj j) (F₃.obj j)

Tactic:
rw [← NatTrans.comp_app, ← NatTrans.comp_app, assoc, associator_hom_snd_fst, assoc]

Result:
case h_snd.h_fst
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (fst (F₁ ⊗ F₂) F₃ ≫ snd F₁ F₂).app j =
    (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j) ≫ fst (F₂.obj j) (F₃.obj j)

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (α_ F₁ F₂ F₃).hom.app j = (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom

Tactic:
apply hom_ext

Result:
case h_fst
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (α_ F₁ F₂ F₃).hom.app j ≫ fst (F₁.obj j) ((F₂ ⊗ F₃).obj j) =
    (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ fst (F₁.obj j) ((F₂ ⊗ F₃).obj j)

case h_snd
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (α_ F₁ F₂ F₃).hom.app j ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j) =
    (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j)
-- Mathlib/Algebra/Order/Floor.lean
theorem preimage_Ico {a b : α} : ((↑) : ℤ → α) ⁻¹' Set.Ico a b = Set.Ico ⌈a⌉ ⌈b⌉

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Ico a b ↔ x✝ ∈ Ico ⌈a⌉ ⌈b⌉

Tactic:
simp [ceil_le, lt_ceil]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ Int.cast ⁻¹' Ico a b = Ico ⌈a⌉ ⌈b⌉

Tactic:
ext

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Ico a b ↔ x✝ ∈ Ico ⌈a⌉ ⌈b⌉
-- Mathlib/Analysis/Convex/Side.lean
theorem _root_.Wbtw.wOppSide₁₃ {s : AffineSubspace R P} {x y z : P} (h : Wbtw R x y z)
    (hy : y ∈ s) : s.WOppSide x z

Proof state:
case intro.intro.intro.inl.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
ht0 : 0 ≤ 0
ht1 : 0 ≤ 1
hy : (lineMap x z) 0 ∈ s
ht1' : 0 < 1
⊢ SameRay R (x -ᵥ (lineMap x z) 0) ((lineMap x z) 0 -ᵥ z)

Tactic:
rw [lineMap_apply_zero]

Result:
case intro.intro.intro.inl.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
ht0 : 0 ≤ 0
ht1 : 0 ≤ 1
hy : (lineMap x z) 0 ∈ s
ht1' : 0 < 1
⊢ SameRay R (x -ᵥ x) (x -ᵥ z)

Proof state:
case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : (lineMap x z) t ∈ s
ht1' : t < 1
ht0' : 0 < t
⊢ (1 - t) • (0 - t • (z -ᵥ x)) = t • (t • (z -ᵥ x) + -(z -ᵥ x))

Tactic:
module

Result:
no goals

Proof state:
case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : (lineMap x z) t ∈ s
ht1' : t < 1
ht0' : 0 < t
⊢ SameRay R (x -ᵥ (lineMap x z) t) ((lineMap x z) t -ᵥ z)

case intro.intro.intro.inl.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
ht0 : 0 ≤ 0
ht1 : 0 ≤ 1
hy : (lineMap x z) 0 ∈ s
ht1' : 0 < 1
⊢ SameRay R (x -ᵥ (lineMap x z) 0) ((lineMap x z) 0 -ᵥ z)

Tactic:
swap

Result:
case intro.intro.intro.inl.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
ht0 : 0 ≤ 0
ht1 : 0 ≤ 1
hy : (lineMap x z) 0 ∈ s
ht1' : 0 < 1
⊢ SameRay R (x -ᵥ (lineMap x z) 0) ((lineMap x z) 0 -ᵥ z)

case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : (lineMap x z) t ∈ s
ht1' : t < 1
ht0' : 0 < t
⊢ SameRay R (x -ᵥ (lineMap x z) t) ((lineMap x z) t -ᵥ z)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem countP_toList (as : Array α) : as.toList.countP p = countP p as

Proof state:
α : Type u_1
p : α → Bool
as : Array α
⊢ List.countP p as.toList = countP p as

Tactic:
cases as

Result:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ List.countP p { toList := toList✝ }.toList = countP p { toList := toList✝ }

Proof state:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ List.countP p { toList := toList✝ }.toList = countP p { toList := toList✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem xn_modEq_x4n_add (n j) : xn a1 (4 * n + j) ≡ xn a1 j [MOD xn a1 n] :=
  ModEq.add_right_cancel' (xn a1 (2 * n + j)) <| by
    refine @ModEq.trans _ _ 0 _ ?_ (by rw [add_comm]; exact (xn_modEq_x2n_add _ _ _).symm)
    rw [show 4 * n = 2 * n + 2 * n from right_distrib 2 2 n, add_assoc]
    apply xn_modEq_x2n_add

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ xn a1 (2 * n + (2 * n + j)) + xn a1 (2 * n + j) ≡ 0 [MOD xn a1 n]

Tactic:
apply xn_modEq_x2n_add

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ xn a1 (4 * n + j) + xn a1 (2 * n + j) ≡ 0 [MOD xn a1 n]

Tactic:
rw [show 4 * n = 2 * n + 2 * n from right_distrib 2 2 n, add_assoc]

Result:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ xn a1 (2 * n + (2 * n + j)) + xn a1 (2 * n + j) ≡ 0 [MOD xn a1 n]

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ xn a1 (4 * n + j) + xn a1 (2 * n + j) ≡ xn a1 j + xn a1 (2 * n + j) [MOD xn a1 n]

Tactic:
refine @ModEq.trans _ _ 0 _ ?_ (by rw [add_comm]; exact (xn_modEq_x2n_add _ _ _).symm)

Result:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ xn a1 (4 * n + j) + xn a1 (2 * n + j) ≡ 0 [MOD xn a1 n]

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ 0 ≡ xn a1 j + xn a1 (2 * n + j) [MOD xn a1 n]

Tactic:
rw [add_comm]

Result:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ 0 ≡ xn a1 (2 * n + j) + xn a1 j [MOD xn a1 n]

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ 0 ≡ xn a1 (2 * n + j) + xn a1 j [MOD xn a1 n]

Tactic:
exact (xn_modEq_x2n_add _ _ _).symm

Result:
no goals
-- Mathlib/Order/Hom/CompleteLattice.lean
theorem map_iInf₂ [InfSet α] [InfSet β] [sInfHomClass F α β] (f : F) (g : ∀ i, κ i → α) :
    f (⨅ (i) (j), g i j) = ⨅ (i) (j), f (g i j)

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : FunLike F α β
inst✝² : InfSet α
inst✝¹ : InfSet β
inst✝ : sInfHomClass F α β
f : F
g : (i : ι) → κ i → α
⊢ f (⨅ i, ⨅ j, g i j) = ⨅ i, ⨅ j, f (g i j)

Tactic:
simp_rw [map_iInf]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Symmetric.lean
@[aesop safe apply]
lemma IsSymmetric.pow {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (n : ℕ) : (T ^ n).IsSymmetric

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
n : ℕ
⊢ (T ^ 0).IsSymmetric

Tactic:
simp [one_eq_id]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
n : ℕ
⊢ (T ^ n).IsSymmetric

Tactic:
refine Nat.le_induction (by simp [one_eq_id]) (fun k _ ih ↦ ?_) n n.zero_le

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
n k : ℕ
x✝ : 0 ≤ k
ih : (T ^ k).IsSymmetric
⊢ (T ^ (k + 1)).IsSymmetric

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
n k : ℕ
x✝ : 0 ≤ k
ih : (T ^ k).IsSymmetric
⊢ IsSymmetric (T ^ k * T)

Tactic:
exact ih.mul_of_commute hT <| .pow_left rfl k

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
n k : ℕ
x✝ : 0 ≤ k
ih : (T ^ k).IsSymmetric
⊢ (T ^ (k + 1)).IsSymmetric

Tactic:
rw [iterate_succ, ← mul_eq_comp]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
n k : ℕ
x✝ : 0 ≤ k
ih : (T ^ k).IsSymmetric
⊢ IsSymmetric (T ^ k * T)