harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem dNext_cochainComplex (f : ∀ i j, P.X i ⟶ Q.X j) (j : ℕ) :
    dNext j f = P.d _ _ ≫ f (j + 1) j

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
j : ℕ
⊢ P.d j ((ComplexShape.up ℕ).next j) ≫ f ((ComplexShape.up ℕ).next j) j = P.d j (j + 1) ≫ f (j + 1) j

Tactic:
have : (ComplexShape.up ℕ).next j = j + 1 := CochainComplex.next ℕ j

Result:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
j : ℕ
this : (ComplexShape.up ℕ).next j = j + 1
⊢ P.d j ((ComplexShape.up ℕ).next j) ≫ f ((ComplexShape.up ℕ).next j) j = P.d j (j + 1) ≫ f (j + 1) j

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
j : ℕ
⊢ (dNext j) f = P.d j (j + 1) ≫ f (j + 1) j

Tactic:
dsimp [dNext]

Result:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
j : ℕ
⊢ P.d j ((ComplexShape.up ℕ).next j) ≫ f ((ComplexShape.up ℕ).next j) j = P.d j (j + 1) ≫ f (j + 1) j

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
j : ℕ
this : (ComplexShape.up ℕ).next j = j + 1
⊢ P.d j ((ComplexShape.up ℕ).next j) ≫ f ((ComplexShape.up ℕ).next j) j = P.d j (j + 1) ≫ f (j + 1) j

Tactic:
congr 2

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Basic.lean
theorem GradedAlgebra.proj_recompose (a : ⨁ i, 𝒜 i) (i : ι) :
    GradedAlgebra.proj 𝒜 i ((decompose 𝒜).symm a) = (decompose 𝒜).symm (of _ i (a i))

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
⊢ (proj 𝒜 i) ((decompose 𝒜).symm a) = (decompose 𝒜).symm ((of (fun i => ↥(𝒜 i)) i) (a i))

Tactic:
rw [GradedAlgebra.proj_apply, decompose_symm_of, Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/FractionalIdeal.lean
theorem fractionalIdeal_rank (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ) :
    finrank ℤ I = finrank ℤ (𝓞 K)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ finrank ℤ ↥↑↑I = finrank ℤ (𝓞 K)

Tactic:
rw [finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank,
  finrank_eq_card_basis (basisOfFractionalIdeal K I)]

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_varsToConstants [L[[α]].Structure M] [(lhomWithConstants L α).IsExpansionOn M]
    {t : L.Term (α ⊕ β)} {v : β → M} :
    t.varsToConstants.realize v = t.realize (Sum.elim (fun a => ↑(L.con a)) v)

Proof state:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
t : L.Term (α ⊕ β)
v : β → M
⊢ realize v t.varsToConstants = realize (Sum.elim (fun a => ↑(L.con a)) v) t

Tactic:
induction' t with ab n f ts ih

Result:
case var
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
ab : α ⊕ β
⊢ realize v (var ab).varsToConstants = realize (Sum.elim (fun a => ↑(L.con a)) v) (var ab)

case func
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
n : ℕ
f : L.Functions n
ts : Fin n → L.Term (α ⊕ β)
ih : ∀ (a : Fin n), realize v (ts a).varsToConstants = realize (Sum.elim (fun a => ↑(L.con a)) v) (ts a)
⊢ realize v (func f ts).varsToConstants = realize (Sum.elim (fun a => ↑(L.con a)) v) (func f ts)

Proof state:
case func
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
n : ℕ
f : L.Functions n
ts : Fin n → L.Term (α ⊕ β)
ih : ∀ (a : Fin n), realize v (ts a).varsToConstants = realize (Sum.elim (fun a => ↑(L.con a)) v) (ts a)
⊢ (funMap (Sum.inl f) fun i => realize (Sum.elim (fun a => ↑(L.con a)) v) (ts i)) =
    funMap f fun i => realize (Sum.elim (fun a => ↑(L.con a)) v) (ts i)

Tactic:
rw [withConstants_funMap_sumInl]

Result:
no goals

Proof state:
case func
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
n : ℕ
f : L.Functions n
ts : Fin n → L.Term (α ⊕ β)
ih : ∀ (a : Fin n), realize v (ts a).varsToConstants = realize (Sum.elim (fun a => ↑(L.con a)) v) (ts a)
⊢ realize v (func f ts).varsToConstants = realize (Sum.elim (fun a => ↑(L.con a)) v) (func f ts)

Tactic:
simp only [realize, constantsOn, constantsOnFunc, ih, varsToConstants]

Result:
case func
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
n : ℕ
f : L.Functions n
ts : Fin n → L.Term (α ⊕ β)
ih : ∀ (a : Fin n), realize v (ts a).varsToConstants = realize (Sum.elim (fun a => ↑(L.con a)) v) (ts a)
⊢ (funMap (Sum.inl f) fun i => realize (Sum.elim (fun a => ↑(L.con a)) v) (ts i)) =
    funMap f fun i => realize (Sum.elim (fun a => ↑(L.con a)) v) (ts i)

Proof state:
case var
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
ab : α ⊕ β
⊢ realize v (var ab).varsToConstants = realize (Sum.elim (fun a => ↑(L.con a)) v) (var ab)

Tactic:
rcases ab with a | b <;> simp [Language.con]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma IsMeasurableRatCDF.measure_stieltjesFunction_univ (a : α) :
    (hf.stieltjesFunction a).measure univ = 1

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
⊢ (hf.stieltjesFunction a).measure univ = 1

Tactic:
rw [← ENNReal.ofReal_one, ← sub_zero (1 : ℝ)]

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
⊢ (hf.stieltjesFunction a).measure univ = ENNReal.ofReal (1 - 0)

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
⊢ (hf.stieltjesFunction a).measure univ = ENNReal.ofReal (1 - 0)

Tactic:
exact StieltjesFunction.measure_univ _ (tendsto_stieltjesFunction_atBot hf a)
  (tendsto_stieltjesFunction_atTop hf a)

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem t0Space_iff_or_not_mem_closure (X : Type u) [TopologicalSpace X] :
    T0Space X ↔ Pairwise fun a b : X => a ∉ closure ({b} : Set X) ∨ b ∉ closure ({a} : Set X)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
⊢ T0Space X ↔ Pairwise fun a b => a ∉ closure {b} ∨ b ∉ closure {a}

Tactic:
simp only [t0Space_iff_not_inseparable, inseparable_iff_mem_closure, not_and_or]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Spectrum.lean
lemma nnnorm_map (φ : F) (a : A) : ‖φ a‖₊ = ‖a‖₊ :=
  le_antisymm (NonUnitalStarAlgHom.nnnorm_apply_le φ a) <| by
    simpa using NonUnitalStarAlgHom.nnnorm_apply_le (symm (φ : A ≃⋆ₐ[ℂ] B)) ((φ : A ≃⋆ₐ[ℂ] B) a)

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : EquivLike F A B
inst✝¹ : NonUnitalAlgEquivClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
⊢ ‖a‖₊ ≤ ‖φ a‖₊

Tactic:
simpa using NonUnitalStarAlgHom.nnnorm_apply_le (symm (φ : A ≃⋆ₐ[ℂ] B)) ((φ : A ≃⋆ₐ[ℂ] B) a)

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem continuous_nhdsAdjoint_dom [TopologicalSpace β] {f : α → β} {a : α} {l : Filter α} :
    Continuous[nhdsAdjoint a l, _] f ↔ Tendsto f l (𝓝 (f a))

Proof state:
α : Type u
β : Type v
inst✝ : TopologicalSpace β
f : α → β
a : α
l : Filter α
⊢ Continuous f ↔ Tendsto f l (𝓝 (f a))

Tactic:
simp_rw [continuous_iff_le_induced, gc_nhds _ _, nhds_induced, tendsto_iff_comap]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem le_prod_iff {H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} :
    J ≤ H.prod K ↔ map (MonoidHom.fst G N) J ≤ H ∧ map (MonoidHom.snd G N) J ≤ K

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
K : Subgroup N
J : Subgroup (G × N)
⊢ J ≤ H.prod K ↔ map (MonoidHom.fst G N) J ≤ H ∧ map (MonoidHom.snd G N) J ≤ K

Tactic:
simpa only [← Subgroup.toSubmonoid_le] using Submonoid.le_prod_iff

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem pow_mod_card_support_cycleOf_self_apply [DecidableEq α] [Fintype α]
    (f : Perm α) (n : ℕ) (x : α) : (f ^ (n % #(f.cycleOf x).support)) x = (f ^ n) x

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
n : ℕ
x : α
⊢ (f ^ (n % #(f.cycleOf x).support)) x = (f ^ n) x

Tactic:
by_cases hx : f x = x

Result:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
n : ℕ
x : α
hx : f x = x
⊢ (f ^ (n % #(f.cycleOf x).support)) x = (f ^ n) x

case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
n : ℕ
x : α
hx : ¬f x = x
⊢ (f ^ (n % #(f.cycleOf x).support)) x = (f ^ n) x

Proof state:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
n : ℕ
x : α
hx : ¬f x = x
⊢ (f ^ (n % #(f.cycleOf x).support)) x = (f ^ n) x

Tactic:
rw [← cycleOf_pow_apply_self, ← cycleOf_pow_apply_self f, ← (isCycle_cycleOf f hx).orderOf,
  pow_mod_orderOf]

Result:
no goals

Proof state:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
n : ℕ
x : α
hx : f x = x
⊢ (f ^ (n % #(f.cycleOf x).support)) x = (f ^ n) x

Tactic:
rw [pow_apply_eq_self_of_apply_eq_self hx, pow_apply_eq_self_of_apply_eq_self hx]

Result:
no goals
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem hasLineDerivWithinAt_zero : HasLineDerivWithinAt 𝕜 f 0 s x 0

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
s : Set E
x : E
⊢ HasLineDerivWithinAt 𝕜 f 0 s x 0

Tactic:
simp [HasLineDerivWithinAt, hasDerivWithinAt_const]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Permanent.lean
theorem permanent_updateRow_smul (M : Matrix n n R) (j : n) (c : R) (u : n → R) :
    permanent (updateRow M j <| c • u) = c * permanent (updateRow M j u)

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
⊢ (M.updateRow j (c • u)).permanent = c * (M.updateRow j u).permanent

Tactic:
rw [← permanent_transpose, ← updateCol_transpose, permanent_updateCol_smul,
  updateCol_transpose, permanent_transpose]

Result:
no goals
-- Mathlib/NumberTheory/Ostrowski.lean
/-- The equivalence class of an absolute value on the rationals is determined by its values on
the natural numbers. -/
lemma equiv_on_nat_iff_equiv : (∃ c : ℝ, 0 < c ∧ ∀ n : ℕ , f n ^ c = g n) ↔ f ≈ g

Proof state:
f g : AbsoluteValue ℚ ℝ
x✝ : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), f ↑n ^ c = g ↑n
⊢ (fun x => f x ^ c) = ⇑g

Tactic:
ext1 x

Result:
case h
f g : AbsoluteValue ℚ ℝ
x✝ : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), f ↑n ^ c = g ↑n
x : ℚ
⊢ f x ^ c = g x

Proof state:
f g : AbsoluteValue ℚ ℝ
x✝ : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), f ↑n ^ c = g ↑n
x : ℚ
⊢ 0 ≤ f ↑x.num

Tactic:
positivity

Result:
no goals

Proof state:
f g : AbsoluteValue ℚ ℝ
x✝ : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), f ↑n ^ c = g ↑n
x : ℚ
⊢ 0 ≤ f ↑x.den

Tactic:
positivity

Result:
no goals

Proof state:
case h
f g : AbsoluteValue ℚ ℝ
x✝ : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), f ↑n ^ c = g ↑n
x : ℚ
⊢ f x ^ c = g x

Tactic:
rw [← Rat.num_div_den x, map_div₀, map_div₀, div_rpow (by positivity) (by positivity), h x.den,
  ← apply_natAbs_eq,← apply_natAbs_eq, h (natAbs x.num)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem shiftLeftRec_succ {x : BitVec w₁} {y : BitVec w₂} :
    shiftLeftRec x y (n + 1) = (shiftLeftRec x y n) <<< (y &&& twoPow w₂ (n + 1))

Proof state:
w₁ w₂ n : Nat
x : BitVec w₁
y : BitVec w₂
⊢ x.shiftLeftRec y (n + 1) = x.shiftLeftRec y n <<< (y &&& twoPow w₂ (n + 1))

Tactic:
simp [shiftLeftRec]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma ofHom_add (φ₁ φ₂ : F ⟶ G) :
    Cochain.ofHom (φ₁ + φ₂) = Cochain.ofHom φ₁ + Cochain.ofHom φ₂

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ₁ φ₂ : F ⟶ G
⊢ ofHom (φ₁ + φ₂) = ofHom φ₁ + ofHom φ₂

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
/-- See also `Nat.divModEquiv` for a similar statement as an `Equiv`. -/
protected lemma div_mod_unique (h : 0 < b) :
    a / b = d ∧ a % b = c ↔ c + b * d = a ∧ c < b :=
  ⟨fun ⟨e₁, e₂⟩ ↦ e₁ ▸ e₂ ▸ ⟨mod_add_div _ _, mod_lt _ h⟩, fun ⟨h₁, h₂⟩ ↦ h₁ ▸ by
    rw [add_mul_div_left _ _ h, add_mul_mod_self_left]; simp [div_eq_of_lt, mod_eq_of_lt, h₂]⟩

Proof state:
a b c d : ℕ
h : 0 < b
x✝ : c + b * d = a ∧ c < b
h₁ : c + b * d = a
h₂ : c < b
⊢ c / b + d = d ∧ c % b = c

Tactic:
simp [div_eq_of_lt, mod_eq_of_lt, h₂]

Result:
no goals

Proof state:
a b c d : ℕ
h : 0 < b
x✝ : c + b * d = a ∧ c < b
h₁ : c + b * d = a
h₂ : c < b
⊢ (c + b * d) / b = d ∧ (c + b * d) % b = c

Tactic:
rw [add_mul_div_left _ _ h, add_mul_mod_self_left]

Result:
a b c d : ℕ
h : 0 < b
x✝ : c + b * d = a ∧ c < b
h₁ : c + b * d = a
h₂ : c < b
⊢ c / b + d = d ∧ c % b = c
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zipWith_comm (f : α → β → γ) (la : Array α) (lb : Array β) :
    zipWith f la lb = zipWith (fun b a => f a b) lb la

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
toList✝¹ : List α
toList✝ : List β
⊢ zipWith f { toList := toList✝¹ } { toList := toList✝ } =
    zipWith (fun b a => f a b) { toList := toList✝ } { toList := toList✝¹ }

Tactic:
simpa using List.zipWith_comm _ _ _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
la : Array α
lb : Array β
⊢ zipWith f la lb = zipWith (fun b a => f a b) lb la

Tactic:
cases la

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
lb : Array β
toList✝ : List α
⊢ zipWith f { toList := toList✝ } lb = zipWith (fun b a => f a b) lb { toList := toList✝ }

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
lb : Array β
toList✝ : List α
⊢ zipWith f { toList := toList✝ } lb = zipWith (fun b a => f a b) lb { toList := toList✝ }

Tactic:
cases lb

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
toList✝¹ : List α
toList✝ : List β
⊢ zipWith f { toList := toList✝¹ } { toList := toList✝ } =
    zipWith (fun b a => f a b) { toList := toList✝ } { toList := toList✝¹ }
-- Mathlib/Tactic/Ring/Basic.lean
theorem natCast_nat (n) : ((Nat.rawCast n : ℕ) : R) = Nat.rawCast n

Proof state:
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
⊢ ↑n.rawCast = n.rawCast

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem modifyHead_eq_modify_zero (f : α → α) (l : List α) :
    l.modifyHead f = l.modify f 0

Proof state:
α : Type u_1
f : α → α
l : List α
⊢ modifyHead f l = modify f 0 l

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
theorem w {A B : StructuredArrow S T} (f : A ⟶ B) : A.hom ≫ T.map f.right = B.hom

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
A B : StructuredArrow S T
f : A ⟶ B
this : (Functor.fromPUnit S).map f.left ≫ B.hom = A.hom ≫ T.map f.right
⊢ A.hom ≫ T.map f.right = B.hom

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
A B : StructuredArrow S T
f : A ⟶ B
⊢ A.hom ≫ T.map f.right = B.hom

Tactic:
have := f.w

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
A B : StructuredArrow S T
f : A ⟶ B
this : (Functor.fromPUnit S).map f.left ≫ B.hom = A.hom ≫ T.map f.right
⊢ A.hom ≫ T.map f.right = B.hom
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem finite_quotient_span_sub_one [hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) :
    Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
this : NumberField K
⊢ Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})

Tactic:
refine Fintype.finite <| Ideal.fintypeQuotientOfFreeOfNeBot _ (fun h ↦ ?_)

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
this : NumberField K
h : Ideal.span {hζ.toInteger - 1} = ⊥
⊢ False

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
this : NumberField K
h : Ideal.span {hζ.toInteger - 1} = ⊥
⊢ False

Tactic:
simp only [Ideal.span_singleton_eq_bot, sub_eq_zero, ← Subtype.coe_inj] at h

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
this : NumberField K
h : hζ.toInteger = 1
⊢ False

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
⊢ Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})

Tactic:
have : NumberField K := IsCyclotomicExtension.numberField {p ^ (k + 1)} ℚ K

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
this : NumberField K
⊢ Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
this : NumberField K
h : hζ.toInteger = 1
⊢ False

Tactic:
exact hζ.ne_one (one_lt_pow₀ hp.1.one_lt (Nat.zero_ne_add_one k).symm)
  (RingOfIntegers.ext_iff.1 h)

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem aux_hasSum_of_le_geometric : HasSum (fun n : ℕ ↦ C * r ^ n) (C / (1 - r))

Proof state:
case inr.intro
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
left✝ : 0 < C
r₀ : 0 ≤ r
⊢ HasSum (fun n => C * r ^ n) (C / (1 - r))

Tactic:
refine HasSum.mul_left C ?_

Result:
case inr.intro
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
left✝ : 0 < C
r₀ : 0 ≤ r
⊢ HasSum (HPow.hPow r) (1 - r)⁻¹

Proof state:
case inr.intro
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
left✝ : 0 < C
r₀ : 0 ≤ r
⊢ HasSum (HPow.hPow r) (1 - r)⁻¹

Tactic:
simpa using hasSum_geometric_of_lt_one r₀ hr

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : PseudoMetricSpace α
r : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ 0 * r ^ n
⊢ HasSum (fun n => 0 * r ^ n) (0 / (1 - r))

Tactic:
simp [hasSum_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ HasSum (fun n => C * r ^ n) (C / (1 - r))

Tactic:
rcases sign_cases_of_C_mul_pow_nonneg fun n ↦ dist_nonneg.trans (hu n) with (rfl | ⟨_, r₀⟩)

Result:
case inl
α : Type u_1
inst✝ : PseudoMetricSpace α
r : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ 0 * r ^ n
⊢ HasSum (fun n => 0 * r ^ n) (0 / (1 - r))

case inr.intro
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
left✝ : 0 < C
r₀ : 0 ≤ r
⊢ HasSum (fun n => C * r ^ n) (C / (1 - r))
-- Mathlib/Data/Nat/Sqrt.lean
lemma sqrt_eq_zero : sqrt n = 0 ↔ n = 0 :=
  ⟨fun h ↦
      Nat.eq_zero_of_le_zero <| le_of_lt_succ <| (@sqrt_lt n 1).1 <| by rw [h]; decide,
    by rintro rfl; simp⟩

Proof state:
n : ℕ
⊢ n = 0 → n.sqrt = 0

Tactic:
rintro rfl

Result:
⊢ sqrt 0 = 0

Proof state:
n : ℕ
h : n.sqrt = 0
⊢ n.sqrt < 1

Tactic:
rw [h]

Result:
n : ℕ
h : n.sqrt = 0
⊢ 0 < 1

Proof state:
n : ℕ
h : n.sqrt = 0
⊢ 0 < 1

Tactic:
decide

Result:
no goals

Proof state:
⊢ sqrt 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive sum_nsmul_assoc]
lemma prod_pow_eq_pow_sum (s : Finset ι) (f : ι → ℕ) (a : β) :
    ∏ i ∈ s, a ^ f i = a ^ ∑ i ∈ s, f i :=
  cons_induction (by simp) (fun _ _ _ _ ↦ by simp [prod_cons, sum_cons, pow_add, *]) s

Proof state:
ι : Type u_1
β : Type u_4
inst✝ : CommMonoid β
s : Finset ι
f : ι → ℕ
a : β
x✝³ : ι
x✝² : Finset ι
x✝¹ : x✝³ ∉ x✝²
x✝ : ∏ i ∈ x✝², a ^ f i = a ^ ∑ i ∈ x✝², f i
⊢ ∏ i ∈ cons x✝³ x✝² x✝¹, a ^ f i = a ^ ∑ i ∈ cons x✝³ x✝² x✝¹, f i

Tactic:
simp [prod_cons, sum_cons, pow_add, *]

Result:
no goals

Proof state:
ι : Type u_1
β : Type u_4
inst✝ : CommMonoid β
s : Finset ι
f : ι → ℕ
a : β
⊢ ∏ i ∈ ∅, a ^ f i = a ^ ∑ i ∈ ∅, f i

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Hermitian.lean
theorem IsHermitian.adjugate [Fintype m] [DecidableEq m] {A : Matrix m m α} (hA : A.IsHermitian) :
    A.adjugate.IsHermitian

Proof state:
α : Type u_1
m : Type u_3
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
hA : A.IsHermitian
⊢ A.adjugate.IsHermitian

Tactic:
simp [IsHermitian, adjugate_conjTranspose, hA.eq]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Quotient.lean
theorem isClosedMap_coe {H : Subgroup G} (hH : IsCompact (H : Set G)) :
    IsClosedMap ((↑) : G → G ⧸ H)

Proof state:
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : Subgroup G
hH : IsCompact ↑H
t : Set G
ht : IsClosed t
⊢ IsClosed (mk '' t)

Tactic:
rw [← (isQuotientMap_mk H).isClosed_preimage, preimage_image_mk_eq_mul]

Result:
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : Subgroup G
hH : IsCompact ↑H
t : Set G
ht : IsClosed t
⊢ IsClosed (t * ↑H)

Proof state:
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : Subgroup G
hH : IsCompact ↑H
⊢ IsClosedMap mk

Tactic:
intro t ht

Result:
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : Subgroup G
hH : IsCompact ↑H
t : Set G
ht : IsClosed t
⊢ IsClosed (mk '' t)

Proof state:
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : Subgroup G
hH : IsCompact ↑H
t : Set G
ht : IsClosed t
⊢ IsClosed (t * ↑H)

Tactic:
exact ht.mul_right_of_isCompact hH

Result:
no goals
-- Mathlib/Data/Finsupp/Fin.lean
theorem cons_ne_zero_of_right (h : s ≠ 0) : cons y s ≠ 0

Proof state:
case h
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
c : cons y s = 0
a : Fin n
⊢ s a = 0 a

Tactic:
simp [← cons_succ a y s, c]

Result:
no goals

Proof state:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
c : cons y s = 0
⊢ s = 0

Tactic:
ext a

Result:
case h
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
c : cons y s = 0
a : Fin n
⊢ s a = 0 a

Proof state:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
h : s ≠ 0
⊢ cons y s ≠ 0

Tactic:
contrapose! h with c

Result:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
c : cons y s = 0
⊢ s = 0