harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/DirectSum/Internal.lean
theorem SetLike.intCast_mem_graded [Zero ι] [AddGroupWithOne R] [SetLike σ R]
    [AddSubgroupClass σ R] (A : ι → σ) [SetLike.GradedOne A] (z : ℤ) : (z : R) ∈ A 0

Proof state:
case negSucc
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ -↑(a✝ + 1) ∈ A 0

Tactic:
exact neg_mem (SetLike.natCast_mem_graded _ _)

Result:
no goals

Proof state:
case ofNat
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑a✝ ∈ A 0

Tactic:
exact SetLike.natCast_mem_graded _ _

Result:
no goals

Proof state:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
z : ℤ
⊢ ↑z ∈ A 0

Tactic:
cases z

Result:
case ofNat
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑(Int.ofNat a✝) ∈ A 0

case negSucc
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑(Int.negSucc a✝) ∈ A 0

Proof state:
case ofNat
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑(Int.ofNat a✝) ∈ A 0

Tactic:
rw [Int.ofNat_eq_coe, Int.cast_natCast]

Result:
case ofNat
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑a✝ ∈ A 0

Proof state:
case negSucc
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑(Int.negSucc a✝) ∈ A 0

Tactic:
rw [Int.cast_negSucc]

Result:
case negSucc
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ -↑(a✝ + 1) ∈ A 0
-- Mathlib/Data/Finsupp/AList.lean
theorem lookupFinsupp_apply [DecidableEq α] (l : AList fun _x : α => M) (a : α) :
    l.lookupFinsupp a = (l.lookup a).getD 0

Proof state:
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
⊢ l.lookupFinsupp a = (lookup a l).getD 0

Tactic:
convert rfl

Result:
case h.e'_3
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
⊢ (lookup a l).getD 0 = l.lookupFinsupp a

Proof state:
case h.e'_3
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
⊢ (lookup a l).getD 0 = l.lookupFinsupp a

Tactic:
congr

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem getElem_zipIdx (a : Vector α n) (i : Nat) (h : i < n) :
    (a.zipIdx k)[i] = (a[i]'(by simp_all), k + i)

Proof state:
α : Type ?u.9958
n k : Nat
a : Vector α n
i : Nat
h : i < n
⊢ i < n

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
n k : Nat
a : Vector α n
i : Nat
h : i < n
⊢ (a.zipIdx k)[i] = (a[i], k + i)

Tactic:
rcases a with ⟨a, rfl⟩

Result:
case mk
α : Type u_1
k i : Nat
a : Array α
h : i < a.size
⊢ ({ toArray := a, size_toArray := ⋯ }.zipIdx k)[i] = ({ toArray := a, size_toArray := ⋯ }[i], k + i)

Proof state:
case mk
α : Type u_1
k i : Nat
a : Array α
h : i < a.size
⊢ ({ toArray := a, size_toArray := ⋯ }.zipIdx k)[i] = ({ toArray := a, size_toArray := ⋯ }[i], k + i)

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
theorem rightCosetEquivalence_equiv_snd (g : G) :
    RightCosetEquivalence H g ((hHT.equiv g).snd : G)

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g : G
⊢ RightCosetEquivalence (↑H) g ↑(hHT.equiv g).2

Tactic:
rw [RightCosetEquivalence, rightCoset_eq_iff, equiv_snd_eq_inv_mul]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g : G
⊢ (↑(hHT.equiv g).1)⁻¹ * g * g⁻¹ ∈ H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g : G
⊢ (↑(hHT.equiv g).1)⁻¹ * g * g⁻¹ ∈ H

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Basic.lean
theorem one_mul (χ : MulChar R R') : (1 : MulChar R R') * χ = χ

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
⊢ 1 * χ = χ

Tactic:
ext

Result:
case h
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a✝ : Rˣ
⊢ (1 * χ) ↑a✝ = χ ↑a✝

Proof state:
case h
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a✝ : Rˣ
⊢ (1 * χ) ↑a✝ = χ ↑a✝

Tactic:
simp only [one_mul, Pi.mul_apply, MulChar.coeToFun_mul, MulChar.one_apply_coe]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean
theorem integral_exp_Iic (c : ℝ) : ∫ x : ℝ in Iic c, exp x = exp c

Proof state:
c : ℝ
⊢ ∫ (x : ℝ) in Iic c, rexp x = rexp c

Tactic:
refine
  tendsto_nhds_unique
    (intervalIntegral_tendsto_integral_Iic _ (integrableOn_exp_Iic _) tendsto_id) ?_

Result:
c : ℝ
⊢ Tendsto (fun i => ∫ (x : ℝ) in id i..c, rexp x) atBot (𝓝 (rexp c))

Proof state:
c : ℝ
⊢ 𝓝 (rexp c) = 𝓝 (rexp c - 0)

Tactic:
rw [sub_zero]

Result:
no goals

Proof state:
c : ℝ
⊢ Tendsto (fun i => ∫ (x : ℝ) in id i..c, rexp x) atBot (𝓝 (rexp c))

Tactic:
simp_rw [integral_exp, show 𝓝 (exp c) = 𝓝 (exp c - 0) by rw [sub_zero]]

Result:
c : ℝ
⊢ Tendsto (fun i => rexp c - rexp (id i)) atBot (𝓝 (rexp c - 0))

Proof state:
c : ℝ
⊢ Tendsto (fun i => rexp c - rexp (id i)) atBot (𝓝 (rexp c - 0))

Tactic:
exact tendsto_exp_atBot.const_sub _

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem single_zero_smul_eq_smul (Γ) [OrderedAddCommMonoid Γ] [AddAction Γ Γ']
    [IsOrderedCancelVAdd Γ Γ'] [MulZeroClass R] [SMulWithZero R V] {r : R}
    {x : HahnModule Γ' R V} :
    (HahnSeries.single (0 : Γ) r) • x = r • x

Proof state:
case h.h
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ'
inst✝⁵ : AddCommMonoid V
Γ : Type u_6
inst✝⁴ : OrderedAddCommMonoid Γ
inst✝³ : AddAction Γ Γ'
inst✝² : IsOrderedCancelVAdd Γ Γ'
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
x✝ : Γ'
⊢ ((of R).symm ((HahnSeries.single 0) r • x)).coeff x✝ = ((of R).symm (r • x)).coeff x✝

Tactic:
exact coeff_single_zero_smul

Result:
no goals

Proof state:
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ'
inst✝⁵ : AddCommMonoid V
Γ : Type u_6
inst✝⁴ : OrderedAddCommMonoid Γ
inst✝³ : AddAction Γ Γ'
inst✝² : IsOrderedCancelVAdd Γ Γ'
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
⊢ (HahnSeries.single 0) r • x = r • x

Tactic:
ext

Result:
case h.h
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ'
inst✝⁵ : AddCommMonoid V
Γ : Type u_6
inst✝⁴ : OrderedAddCommMonoid Γ
inst✝³ : AddAction Γ Γ'
inst✝² : IsOrderedCancelVAdd Γ Γ'
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
x✝ : Γ'
⊢ ((of R).symm ((HahnSeries.single 0) r • x)).coeff x✝ = ((of R).symm (r • x)).coeff x✝
-- Mathlib/Topology/Algebra/Module/Basic.lean
theorem Submodule.dense_iff_topologicalClosure_eq_top {s : Submodule R M} :
    Dense (s : Set M) ↔ s.topologicalClosure = ⊤

Proof state:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousAdd M
s : Submodule R M
⊢ closure ↑s = Set.univ ↔ ↑s.topologicalClosure = ↑⊤

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousAdd M
s : Submodule R M
⊢ Dense ↑s ↔ s.topologicalClosure = ⊤

Tactic:
rw [← SetLike.coe_set_eq, dense_iff_closure_eq]

Result:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousAdd M
s : Submodule R M
⊢ closure ↑s = Set.univ ↔ ↑s.topologicalClosure = ↑⊤
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_shrink (a : Array α) (n : Nat) : (a.shrink n).size = min n a.size

Proof state:
α : Type u_1
a : Array α
n : Nat
⊢ a.size - (a.size - n) = min n a.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
a : Array α
n : Nat
⊢ (a.shrink n).size = min n a.size

Tactic:
simp [shrink]

Result:
α : Type u_1
a : Array α
n : Nat
⊢ a.size - (a.size - n) = min n a.size
-- Mathlib/Topology/UnitInterval.lean
theorem continuous_symm : Continuous σ

Proof state:
⊢ Continuous σ

Tactic:
apply Continuous.subtype_mk (by fun_prop)

Result:
no goals

Proof state:
⊢ Continuous fun x => 1 - ↑x

Tactic:
fun_prop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem foldr_subtype {p : α → Prop} {l : Array { x // p x }}
    {f : { x // p x } → β → β} {g : α → β → β} {x : β}
    (hf : ∀ x h b, f ⟨x, h⟩ b = g x b) :
    l.foldr f x = l.unattach.foldr g x

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → β → β
g : α → β → β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
toList✝ : List { x // p x }
⊢ foldr f x { toList := toList✝ } = foldr g x { toList := toList✝ }.unattach

Tactic:
simp only [List.foldr_toArray', List.unattach_toArray]

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → β → β
g : α → β → β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
toList✝ : List { x // p x }
⊢ List.foldr f x toList✝ = List.foldr g x toList✝.unattach

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → β → β
g : α → β → β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
toList✝ : List { x // p x }
⊢ ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b

Tactic:
simp [hf]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → β → β
g : α → β → β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
toList✝ : List { x // p x }
⊢ List.foldr f x toList✝ = List.foldr g x toList✝.unattach

Tactic:
rw [List.foldr_subtype]

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → β → β
g : α → β → β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
toList✝ : List { x // p x }
⊢ ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
l : Array { x // p x }
f : { x // p x } → β → β
g : α → β → β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
⊢ foldr f x l = foldr g x l.unattach

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → β → β
g : α → β → β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
toList✝ : List { x // p x }
⊢ foldr f x { toList := toList✝ } = foldr g x { toList := toList✝ }.unattach
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
@[simp] lemma _root_.Equiv.simpleGraph_refl : (Equiv.refl V).simpleGraph = Equiv.refl _

Proof state:
V : Type u_1
⊢ (Equiv.refl V).simpleGraph = Equiv.refl (SimpleGraph V)

Tactic:
ext

Result:
case H.Adj.h.h.a
V : Type u_1
x✝² : SimpleGraph V
x✝¹ x✝ : V
⊢ ((Equiv.refl V).simpleGraph x✝²).Adj x✝¹ x✝ ↔ ((Equiv.refl (SimpleGraph V)) x✝²).Adj x✝¹ x✝

Proof state:
case H.Adj.h.h.a
V : Type u_1
x✝² : SimpleGraph V
x✝¹ x✝ : V
⊢ ((Equiv.refl V).simpleGraph x✝²).Adj x✝¹ x✝ ↔ ((Equiv.refl (SimpleGraph V)) x✝²).Adj x✝¹ x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean
lemma isHamiltonianCycle_iff_isCycle_and_support_count_tail_eq_one :
    p.IsHamiltonianCycle ↔ p.IsCycle ∧ ∀ a, (support p).tail.count a = 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
⊢ p.IsHamiltonianCycle ↔ p.IsCycle ∧ ∀ (a_1 : α), List.count a_1 p.support.tail = 1

Tactic:
simp +contextual [isHamiltonianCycle_isCycle_and_isHamiltonian_tail,
  IsHamiltonian, support_tail, IsCycle.not_nil, exists_prop]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem or_of_and_eq_false {a b : Prop} (h : (a ∧ b) = False) : (¬a ∨ ¬b)

Proof state:
a b : Prop
h : (a ∧ b) = False
⊢ ¬a ∨ ¬b

Tactic:
by_cases a <;> by_cases b <;> simp_all

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem map_fromSpec {V : X.Opens} (hV : IsAffineOpen V) (f : op U ⟶ op V) :
    Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this✝ : IsAffine ↑U
this : IsAffine ↑V
⊢ Spec.map (X.presheaf.map f) ≫ hU.fromSpec =
    Spec.map (X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op)) ≫ (↑U).isoSpec.inv ≫ U.ι

Tactic:
rw [fromSpec, isoSpec_inv, Category.assoc, ← Spec.map_comp_assoc, ← Functor.map_comp]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this✝ : IsAffine ↑U
this : IsAffine ↑V
⊢ Spec.map (X.presheaf.map ((eqToHom ⋯).op ≫ f)) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map (X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op)) ≫ (↑U).isoSpec.inv ≫ U.ι

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this✝ : IsAffine ↑U
this : IsAffine ↑V
⊢ Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec

Tactic:
conv_rhs =>
  rw [fromSpec, ← X.homOfLE_ι (V := U) f.unop.le, isoSpec_inv, Category.assoc,
    ← Scheme.isoSpec_inv_naturality_assoc,
    ← Spec.map_comp_assoc, Scheme.homOfLE_appTop, ← Functor.map_comp]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this✝ : IsAffine ↑U
this : IsAffine ↑V
⊢ Spec.map (X.presheaf.map f) ≫ hU.fromSpec =
    Spec.map (X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op)) ≫ (↑U).isoSpec.inv ≫ U.ι

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this : IsAffine ↑U
⊢ Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec

Tactic:
haveI : IsAffine _ := hV

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this✝ : IsAffine ↑U
this : IsAffine ↑V
⊢ Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
⊢ Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec

Tactic:
have : IsAffine U := hU

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this : IsAffine ↑U
⊢ Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this✝ : IsAffine ↑U
this : IsAffine ↑V
⊢ Spec.map (X.presheaf.map ((eqToHom ⋯).op ≫ f)) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map (X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op)) ≫ (↑U).isoSpec.inv ≫ U.ι

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem re_inner_smul_ofReal_smul_self (x : F) {t : ℝ} :
    re ⟪(t : 𝕜) • x, (t : 𝕜) • x⟫ = normSqF x * t * t

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
t : ℝ
⊢ re ⟪↑t • x, ↑t • x⟫_𝕜 = normSq x * t * t

Tactic:
apply ofReal_injective (K := 𝕜)

Result:
case a
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
t : ℝ
⊢ ↑(re ⟪↑t • x, ↑t • x⟫_𝕜) = ↑(normSq x * t * t)

Proof state:
case a
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
t : ℝ
⊢ ↑(re ⟪↑t • x, ↑t • x⟫_𝕜) = ↑(normSq x * t * t)

Tactic:
simp [inner_self_ofReal_re, inner_smul_ofReal_left, inner_smul_ofReal_right, normSq]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Pullback.lean
lemma pullbackShiftFunctorZero_hom_app :
    (shiftFunctorZero _ A).hom.app X =
      (pullbackShiftIso C φ 0 0 (by simp)).hom.app X ≫ (shiftFunctorZero C B).hom.app X

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
⊢ (shiftFunctorZero (PullbackShift C φ) A).hom.app X =
    (pullbackShiftIso C φ 0 0 ⋯).hom.app X ≫ (shiftFunctorZero C B).hom.app X

Tactic:
rw [← cancel_epi ((shiftFunctorZero _ A).inv.app X), Iso.inv_hom_id_app,
  pullbackShiftFunctorZero_inv_app, assoc, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app]

Result:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
⊢ 𝟙 ((𝟭 (PullbackShift C φ)).obj X) = 𝟙 ((𝟭 C).obj X)

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
⊢ 𝟙 ((𝟭 (PullbackShift C φ)).obj X) = 𝟙 ((𝟭 C).obj X)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{?u.7692, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
⊢ 0 = φ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/SeminormFromConst.lean
theorem seminormFromConst_isMul_of_isMul {x : R} (hx : ∀ y : R, f (x * y) = f x * f y) (y : R) :
    seminormFromConst' hf1 hc hpm (x * y) =
      seminormFromConst' hf1 hc hpm x * seminormFromConst' hf1 hc hpm y :=
  have hlim : Tendsto (seminormFromConst_seq c f (x * y)) atTop
      (𝓝 (seminormFromConst' hf1 hc hpm x * seminormFromConst' hf1 hc hpm y))

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
y : R
⊢ Tendsto (seminormFromConst_seq c f (x * y)) atTop (𝓝 (f x * seminormFromConst' hf1 hc hpm y))

Tactic:
have hseq : seminormFromConst_seq c f (x * y) =
    fun n ↦ f x * seminormFromConst_seq c f y n := by
  ext n
  simp only [seminormFromConst_seq, mul_assoc, hx, mul_div_assoc]

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
y : R
hseq : seminormFromConst_seq c f (x * y) = fun n => f x * seminormFromConst_seq c f y n
⊢ Tendsto (seminormFromConst_seq c f (x * y)) atTop (𝓝 (f x * seminormFromConst' hf1 hc hpm y))

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
y : R
⊢ seminormFromConst_seq c f (x * y) = fun n => f x * seminormFromConst_seq c f y n

Tactic:
ext n

Result:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
y : R
n : ℕ
⊢ seminormFromConst_seq c f (x * y) n = f x * seminormFromConst_seq c f y n

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
y : R
hseq : seminormFromConst_seq c f (x * y) = fun n => f x * seminormFromConst_seq c f y n
⊢ Tendsto (seminormFromConst_seq c f (x * y)) atTop (𝓝 (f x * seminormFromConst' hf1 hc hpm y))

Tactic:
simpa [hseq] using (seminormFromConst_isLimit hf1 hc hpm y).const_mul _

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
y : R
⊢ Tendsto (seminormFromConst_seq c f (x * y)) atTop
    (𝓝 (seminormFromConst' hf1 hc hpm x * seminormFromConst' hf1 hc hpm y))

Tactic:
rw [seminormFromConst_apply_of_isMul hf1 hc hpm hx]

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
y : R
⊢ Tendsto (seminormFromConst_seq c f (x * y)) atTop (𝓝 (f x * seminormFromConst' hf1 hc hpm y))

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
y : R
n : ℕ
⊢ seminormFromConst_seq c f (x * y) n = f x * seminormFromConst_seq c f y n

Tactic:
simp only [seminormFromConst_seq, mul_assoc, hx, mul_div_assoc]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma c₄_of_char_two : W.c₄ = W.a₁ ^ 4

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.c₄ = W.a₁ ^ 4

Tactic:
rw [c₄, b₂_of_char_two]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ (W.a₁ ^ 2) ^ 2 - 24 * W.b₄ = W.a₁ ^ 4

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ (W.a₁ ^ 2) ^ 2 - 24 * W.b₄ = W.a₁ ^ 4

Tactic:
linear_combination -12 * W.b₄ * CharP.cast_eq_zero R 2

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
@[simp] lemma div_intCast_re (z : ℂ) (n : ℤ) : (z / n).re = z.re / n

Proof state:
z : ℂ
n : ℤ
⊢ (z / ↑n).re = z.re / ↑n

Tactic:
rw [div_intCast]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem coeff_erase (p : R[X]) (n i : ℕ) :
    (p.erase n).coeff i = if i = n then 0 else p.coeff i

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n i : ℕ
⊢ (erase n p).coeff i = if i = n then 0 else p.coeff i

Tactic:
rcases p with ⟨⟩

Result:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n i : ℕ
toFinsupp✝ : R[ℕ]
⊢ (erase n { toFinsupp := toFinsupp✝ }).coeff i = if i = n then 0 else { toFinsupp := toFinsupp✝ }.coeff i

Proof state:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n i : ℕ
toFinsupp✝ : R[ℕ]
⊢ (Finsupp.erase n toFinsupp✝) i = if i = n then 0 else toFinsupp✝ i

Tactic:
exact ite_congr rfl (fun _ => rfl) (fun _ => rfl)

Result:
no goals

Proof state:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n i : ℕ
toFinsupp✝ : R[ℕ]
⊢ (erase n { toFinsupp := toFinsupp✝ }).coeff i = if i = n then 0 else { toFinsupp := toFinsupp✝ }.coeff i

Tactic:
simp only [erase_def, coeff]

Result:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n i : ℕ
toFinsupp✝ : R[ℕ]
⊢ (Finsupp.erase n toFinsupp✝) i = if i = n then 0 else toFinsupp✝ i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_add (a m n : Nat) : a ^ (m + n) = a ^ m * a ^ n

Proof state:
case zero
a m : Nat
⊢ a ^ (m + 0) = a ^ m * a ^ 0

Tactic:
rw [Nat.add_zero, Nat.pow_zero, Nat.mul_one]

Result:
no goals

Proof state:
a m n : Nat
⊢ a ^ (m + n) = a ^ m * a ^ n

Tactic:
induction n with
| zero => rw [Nat.add_zero, Nat.pow_zero, Nat.mul_one]
| succ _ ih => rw [Nat.add_succ, Nat.pow_succ, Nat.pow_succ, ih, Nat.mul_assoc]

Result:
no goals

Proof state:
case succ
a m n✝ : Nat
ih : a ^ (m + n✝) = a ^ m * a ^ n✝
⊢ a ^ (m + (n✝ + 1)) = a ^ m * a ^ (n✝ + 1)

Tactic:
rw [Nat.add_succ, Nat.pow_succ, Nat.pow_succ, ih, Nat.mul_assoc]

Result:
no goals