harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Monoidal/Center.lean
theorem associator_inv_f (X Y Z : Center C) : Hom.f (α_ X Y Z).inv = (α_ X.1 Y.1 Z.1).inv

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y Z : Center C
⊢ (α_ X Y Z).inv.f = (α_ X.fst Y.fst Z.fst).inv

Tactic:
apply Iso.inv_ext'

Result:
case hom_inv_id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y Z : Center C
⊢ (α_ X.fst Y.fst Z.fst).hom ≫ (α_ X Y Z).inv.f = 𝟙 ((X ⊗ Y) ⊗ Z).fst

Proof state:
case hom_inv_id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y Z : Center C
⊢ (α_ X.fst Y.fst Z.fst).hom ≫ (α_ X Y Z).inv.f = 𝟙 ((X ⊗ Y) ⊗ Z).fst

Tactic:
rw [← associator_hom_f, ← comp_f, Iso.hom_inv_id]

Result:
case hom_inv_id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y Z : Center C
⊢ (𝟙 ((X ⊗ Y) ⊗ Z)).f = 𝟙 ((X ⊗ Y) ⊗ Z).fst

Proof state:
case hom_inv_id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y Z : Center C
⊢ (𝟙 ((X ⊗ Y) ⊗ Z)).f = 𝟙 ((X ⊗ Y) ⊗ Z).fst

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/PNat/Basic.lean
theorem recOn_succ (n : ℕ+) {p : ℕ+ → Sort*} (one succ) :
    @PNat.recOn (n + 1) p one succ = succ n (@PNat.recOn n p one succ)

Proof state:
case mk
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h : 0 < n
⊢ (⟨n, h⟩ + 1).recOn one succ = succ ⟨n, h⟩ (recOn ⟨n, h⟩ one succ)

Tactic:
cases n <;> [exact absurd h (by decide); rfl]

Result:
no goals

Proof state:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
h : 0 < 0
⊢ ¬0 < 0

Tactic:
decide

Result:
no goals

Proof state:
n : ℕ+
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
⊢ (n + 1).recOn one succ = succ n (n.recOn one succ)

Tactic:
obtain ⟨n, h⟩ := n

Result:
case mk
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h : 0 < n
⊢ (⟨n, h⟩ + 1).recOn one succ = succ ⟨n, h⟩ (recOn ⟨n, h⟩ one succ)
-- Mathlib/CategoryTheory/Galois/Decomposition.lean
/-- Up to isomorphism an element of the fiber of `X` only lies in one connected component. -/
lemma connected_component_unique {X A B : C} [IsConnected A] [IsConnected B] (a : F.obj A)
    (b : F.obj B) (i : A ⟶ X) (j : B ⟶ X) (h : F.map i a = F.map j b) [Mono i] [Mono j] :
    ∃ (f : A ≅ B), F.map f.hom a = b

Proof state:
case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).carrier
b : (F.obj B).carrier
i : A ⟶ X
j : B ⟶ X
h : F.map i a = F.map j b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).carrier ≃ { p // F.map i p.1 = F.map j p.2 } := fiberPullbackEquiv F i j
y : (F.obj Y).carrier := e.symm ⟨(a, b), h⟩
hn : IsInitial Y → False
this✝ : IsIso u
this : IsIso v
hu : G.map u y = a
⊢ F.map ((asIso u).symm ≪≫ asIso v).hom a = b

Tactic:
have hv : G.map v y = b := by
  simp only [v, G, y, e, ← PreservesPullback.iso_hom_snd G, fiberPullbackEquiv,
    Iso.toEquiv_comp, Equiv.symm_trans_apply, Iso.toEquiv_symm_fun, types_comp_apply,
    inv_hom_id_apply]
  erw [Types.pullbackIsoPullback_inv_snd_apply (F.map i) (F.map j)]

Result:
case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).carrier
b : (F.obj B).carrier
i : A ⟶ X
j : B ⟶ X
h : F.map i a = F.map j b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).carrier ≃ { p // F.map i p.1 = F.map j p.2 } := fiberPullbackEquiv F i j
y : (F.obj Y).carrier := e.symm ⟨(a, b), h⟩
hn : IsInitial Y → False
this✝ : IsIso u
this : IsIso v
hu : G.map u y = a
hv : G.map v y = b
⊢ F.map ((asIso u).symm ≪≫ asIso v).hom a = b

Proof state:
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).carrier
b : (F.obj B).carrier
i : A ⟶ X
j : B ⟶ X
h : F.map i a = F.map j b
inst✝¹ : Mono i
inst✝ : Mono j
⊢ ∃ f, F.map f.hom a = b

Tactic:
let Y : C := pullback i j

Result:
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).carrier
b : (F.obj B).carrier
i : A ⟶ X
j : B ⟶ X
h : F.map i a = F.map j b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
⊢ ∃ f, F.map f.hom a = b
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem isLimit_sub {a b} (ha : IsLimit a) (h : b < a) : IsLimit (a - b)

Proof state:
a b : Ordinal.{u_4}
ha : a.IsLimit
h : b < a
⊢ b < a ∧ ∀ a_1 < a - b, succ a_1 < a - b

Tactic:
refine ⟨h, fun c hc ↦ ?_⟩

Result:
a b : Ordinal.{u_4}
ha : a.IsLimit
h : b < a
c : Ordinal.{u_4}
hc : c < a - b
⊢ succ c < a - b

Proof state:
a b : Ordinal.{u_4}
ha : a.IsLimit
h : b < a
c : Ordinal.{u_4}
hc : b + c < a
⊢ b + succ c < a

Tactic:
rw [add_succ]

Result:
a b : Ordinal.{u_4}
ha : a.IsLimit
h : b < a
c : Ordinal.{u_4}
hc : b + c < a
⊢ succ (b + c) < a

Proof state:
a b : Ordinal.{u_4}
ha : a.IsLimit
h : b < a
c : Ordinal.{u_4}
hc : c < a - b
⊢ succ c < a - b

Tactic:
rw [lt_sub] at hc ⊢

Result:
a b : Ordinal.{u_4}
ha : a.IsLimit
h : b < a
c : Ordinal.{u_4}
hc : b + c < a
⊢ b + succ c < a

Proof state:
a b : Ordinal.{u_4}
ha : a.IsLimit
h : b < a
c : Ordinal.{u_4}
hc : b + c < a
⊢ succ (b + c) < a

Tactic:
exact ha.succ_lt hc

Result:
no goals

Proof state:
a b : Ordinal.{u_4}
ha : a.IsLimit
h : b < a
⊢ (a - b).IsLimit

Tactic:
rw [isLimit_iff, Ordinal.sub_ne_zero_iff_lt, isSuccPrelimit_iff_succ_lt]

Result:
a b : Ordinal.{u_4}
ha : a.IsLimit
h : b < a
⊢ b < a ∧ ∀ a_1 < a - b, succ a_1 < a - b
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem isLeftInversion_inv_iff {w t : W} :
    cs.IsLeftInversion w⁻¹ t ↔ cs.IsRightInversion w t

Proof state:
case h.e'_2.h.e'_6
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
⊢ w = w⁻¹⁻¹

Tactic:
simp

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
⊢ cs.IsLeftInversion w⁻¹ t ↔ cs.IsRightInversion w t

Tactic:
convert cs.isRightInversion_inv_iff.symm

Result:
case h.e'_2.h.e'_6
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
⊢ w = w⁻¹⁻¹
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
private lemma sum_Icc_mu'_left (a b : α) : ∑ x ∈ Icc a b, mu' 𝕜 x b = if a = b then 1 else 0

Proof state:
case neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab✝ : ¬a = b
hab : ¬a ≤ b
⊢ ∑ x ∈ Icc a b, (IncidenceAlgebra.mu' 𝕜) x b = 0

Tactic:
exact sum_eq_zero fun x hx ↦ apply_eq_zero_of_not_le
  (fun hxb ↦ hab <| (mem_Icc.1 hx).1.trans hxb) _

Result:
no goals

Proof state:
case pos
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab✝ : ¬a = b
hab : a ≤ b
⊢ ∑ x ∈ Icc a b, (IncidenceAlgebra.mu' 𝕜) x b = 0

Tactic:
simp [Icc_eq_cons_Ioc hab, mu'_eq_sum_Ioc_of_ne ‹_›]

Result:
no goals

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ ∑ x ∈ Icc a b, (IncidenceAlgebra.mu' 𝕜) x b = if a = b then 1 else 0

Tactic:
split_ifs with hab

Result:
case pos
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : a = b
⊢ ∑ x ∈ Icc a b, (IncidenceAlgebra.mu' 𝕜) x b = 1

case neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : ¬a = b
⊢ ∑ x ∈ Icc a b, (IncidenceAlgebra.mu' 𝕜) x b = 0

Proof state:
case neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : ¬a = b
⊢ ∑ x ∈ Icc a b, (IncidenceAlgebra.mu' 𝕜) x b = 0

Tactic:
by_cases hab : a ≤ b

Result:
case pos
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab✝ : ¬a = b
hab : a ≤ b
⊢ ∑ x ∈ Icc a b, (IncidenceAlgebra.mu' 𝕜) x b = 0

case neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab✝ : ¬a = b
hab : ¬a ≤ b
⊢ ∑ x ∈ Icc a b, (IncidenceAlgebra.mu' 𝕜) x b = 0

Proof state:
case pos
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : a = b
⊢ ∑ x ∈ Icc a b, (IncidenceAlgebra.mu' 𝕜) x b = 1

Tactic:
simp [hab]

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem tendsto_comp_coe_Ioi_atBot :
    Tendsto (fun x : Ioi a => f x) atBot l ↔ Tendsto f (𝓝[>] a) l

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
l : Filter β
f : α → β
⊢ Tendsto (fun x => f ↑x) atBot l ↔ Tendsto f (𝓝[>] a) l

Tactic:
rw [← map_coe_Ioi_atBot, tendsto_map'_iff]

Result:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
l : Filter β
f : α → β
⊢ Tendsto (fun x => f ↑x) atBot l ↔ Tendsto (f ∘ Subtype.val) atBot l

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
l : Filter β
f : α → β
⊢ Tendsto (fun x => f ↑x) atBot l ↔ Tendsto (f ∘ Subtype.val) atBot l

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean
theorem toTensorAlgebra_gMul {i j} (a : (⨂[R]^i) M) (b : (⨂[R]^j) M) :
    TensorPower.toTensorAlgebra (@GradedMonoid.GMul.mul _ (fun n => ⨂[R]^n M) _ _ _ _ a b) =
      TensorPower.toTensorAlgebra a * TensorPower.toTensorAlgebra b

Proof state:
case H.H.H.H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : Fin i → M
b : Fin j → M
⊢ ((((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra) ((PiTensorProduct.tprod R) a))
      ((PiTensorProduct.tprod R) b) =
    (((LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra) ((PiTensorProduct.tprod R) a))
      ((PiTensorProduct.tprod R) b)

Tactic:
rw [LinearMap.compr₂_apply, ← gMul_eq_coe_linearMap]

Result:
case H.H.H.H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : Fin i → M
b : Fin j → M
⊢ toTensorAlgebra (GradedMonoid.GMul.mul ((PiTensorProduct.tprod R) a) ((PiTensorProduct.tprod R) b)) =
    (((LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra) ((PiTensorProduct.tprod R) a))
      ((PiTensorProduct.tprod R) b)
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
@[simp] lemma induceHom_id (G : SimpleGraph V) (s) :
    induceHom (Hom.id : G →g G) (Set.mapsTo_id s) = Hom.id

Proof state:
case h.a
V : Type u_1
G : SimpleGraph V
s : Set V
x : ↑s
⊢ ↑((induceHom Hom.id ⋯) x) = ↑(Hom.id x)

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
s : Set V
⊢ induceHom Hom.id ⋯ = Hom.id

Tactic:
ext x

Result:
case h.a
V : Type u_1
G : SimpleGraph V
s : Set V
x : ↑s
⊢ ↑((induceHom Hom.id ⋯) x) = ↑(Hom.id x)
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToSimpleFunc_smul_real (T : Set α → E →L[ℝ] F) (h_add : FinMeasAdditive μ T) (c : ℝ)
    {f : α →ₛ E} (hf : Integrable f μ) : setToSimpleFunc T (c • f) = c • setToSimpleFunc T f :=
  calc
    setToSimpleFunc T (c • f) = ∑ x ∈ f.range, T (f ⁻¹' {x}) (c • x)

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
c : ℝ
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ c • 0 = 0

Tactic:
rw [smul_zero]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
c : ℝ
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ setToSimpleFunc T (c • f) = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (c • x)

Tactic:
rw [smul_eq_map c f, map_setToSimpleFunc T h_add hf]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
c : ℝ
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ c • 0 = 0

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
c : ℝ
f : α →ₛ E
hf : Integrable (⇑f) μ
b : E
x✝ : b ∈ f.range
⊢ (T (⇑f ⁻¹' {b})) (c • b) = c • (T (⇑f ⁻¹' {b})) b

Tactic:
rw [ContinuousLinearMap.map_smul (T (f ⁻¹' {b})) c b]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
c : ℝ
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ ∑ x ∈ f.range, c • (T (⇑f ⁻¹' {x})) x = c • setToSimpleFunc T f

Tactic:
simp only [setToSimpleFunc, smul_sum, smul_smul, mul_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem leftUnitor_inv_braiding (X : C) : (λ_ X).inv ≫ (β_ (𝟙_ C) X).hom = (ρ_ X).inv

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (λ_ X).inv ≫ (β_ (𝟙_ C) X).hom = (ρ_ X).inv

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Divisibility.lean
/-- `∣` is not a useful definition if an inverse is available. -/
@[simp]
lemma GroupWithZero.dvd_iff {m n : α} : m ∣ n ↔ (m = 0 → n = 0)

Proof state:
case refine_1
α : Type u_1
inst✝ : GroupWithZero α
m n : α
x✝ : m ∣ n
hm : m = 0
a : α
ha : n = m * a
⊢ n = 0

Tactic:
simp [hm, ha]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : GroupWithZero α
m n : α
h : m = 0 → n = 0
⊢ n = m * (m⁻¹ * n)

Tactic:
obtain rfl | hn := eq_or_ne n 0

Result:
case refine_2.inl
α : Type u_1
inst✝ : GroupWithZero α
m : α
h : m = 0 → 0 = 0
⊢ 0 = m * (m⁻¹ * 0)

case refine_2.inr
α : Type u_1
inst✝ : GroupWithZero α
m n : α
h : m = 0 → n = 0
hn : n ≠ 0
⊢ n = m * (m⁻¹ * n)

Proof state:
case refine_2.inr
α : Type u_1
inst✝ : GroupWithZero α
m n : α
h : m = 0 → n = 0
hn : n ≠ 0
⊢ n = m * (m⁻¹ * n)

Tactic:
rw [mul_inv_cancel_left₀ (mt h hn)]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : GroupWithZero α
m n : α
⊢ m ∣ n ↔ m = 0 → n = 0

Tactic:
refine ⟨fun ⟨a, ha⟩ hm => ?_, fun h => ?_⟩

Result:
case refine_1
α : Type u_1
inst✝ : GroupWithZero α
m n : α
x✝ : m ∣ n
hm : m = 0
a : α
ha : n = m * a
⊢ n = 0

case refine_2
α : Type u_1
inst✝ : GroupWithZero α
m n : α
h : m = 0 → n = 0
⊢ m ∣ n

Proof state:
case refine_2.inl
α : Type u_1
inst✝ : GroupWithZero α
m : α
h : m = 0 → 0 = 0
⊢ 0 = m * (m⁻¹ * 0)

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : GroupWithZero α
m n : α
h : m = 0 → n = 0
⊢ m ∣ n

Tactic:
refine ⟨m⁻¹ * n, ?_⟩

Result:
case refine_2
α : Type u_1
inst✝ : GroupWithZero α
m n : α
h : m = 0 → n = 0
⊢ n = m * (m⁻¹ * n)
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_pi : sin π = 0

Proof state:
⊢ ↑0 = 0

Tactic:
simp

Result:
no goals

Proof state:
⊢ sin ↑π = 0

Tactic:
rw [← ofReal_sin, Real.sin_pi]

Result:
⊢ ↑0 = 0
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem le_weightedOrder_mul :
    f.weightedOrder w + g.weightedOrder w ≤ weightedOrder w (f * g)

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑((weight w) d) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
hi : ¬↑((weight w) i) < weightedOrder w f
hj : ↑((weight w) j) < weightedOrder w g
⊢ (coeff R (i, j).1) f * (coeff R (i, j).2) g = 0

Tactic:
rw [coeff_eq_zero_of_lt_weightedOrder w hj, MulZeroClass.mul_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem coprod_map_prod (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (S : Submodule R M)
    (S' : Submodule R M₂) : (Submodule.prod S S').map (LinearMap.coprod f g) = S.map f ⊔ S'.map g :=
  SetLike.coe_injective <| by
    simp only [LinearMap.coprod_apply, Submodule.coe_sup, Submodule.map_coe]
    rw [← Set.image2_add, Set.image2_image_left, Set.image2_image_right]
    exact Set.image_prod fun m m₂ => f m + g m₂

Proof state:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
S : Submodule R M
S' : Submodule R M₂
⊢ ↑(Submodule.map (f.coprod g) (S.prod S')) = ↑(Submodule.map f S ⊔ Submodule.map g S')

Tactic:
simp only [LinearMap.coprod_apply, Submodule.coe_sup, Submodule.map_coe]

Result:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
S : Submodule R M
S' : Submodule R M₂
⊢ (fun a => f a.1 + g a.2) '' ↑(S.prod S') = ⇑f '' ↑S + ⇑g '' ↑S'

Proof state:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
S : Submodule R M
S' : Submodule R M₂
⊢ (fun a => f a.1 + g a.2) '' ↑(S.prod S') = ⇑f '' ↑S + ⇑g '' ↑S'

Tactic:
rw [← Set.image2_add, Set.image2_image_left, Set.image2_image_right]

Result:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
S : Submodule R M
S' : Submodule R M₂
⊢ (fun a => f a.1 + g a.2) '' ↑(S.prod S') = Set.image2 (fun a b => f a + g b) ↑S ↑S'

Proof state:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
S : Submodule R M
S' : Submodule R M₂
⊢ (fun a => f a.1 + g a.2) '' ↑(S.prod S') = Set.image2 (fun a b => f a + g b) ↑S ↑S'

Tactic:
exact Set.image_prod fun m m₂ => f m + g m₂

Result:
no goals
-- Mathlib/Topology/SeparatedMap.lean
theorem eqOn_of_comp_eqOn (hs : IsPreconnected s) (h₁ : ContinuousOn g₁ s) (h₂ : ContinuousOn g₂ s)
    (he : s.EqOn (p ∘ g₁) (p ∘ g₂)) {a : A} (has : a ∈ s) (ha : g₁ a = g₂ a) : s.EqOn g₁ g₂

Proof state:
X : Type u_1
E : Type u_2
A : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace A
p : E → X
s : Set A
g₁ g₂ : A → E
sep : IsSeparatedMap p
inj : IsLocallyInjective p
hs : IsPreconnected s
h₁ : ContinuousOn g₁ s
h₂ : ContinuousOn g₂ s
he : Set.EqOn (p ∘ g₁) (p ∘ g₂) s
a : A
has : a ∈ s
ha : g₁ a = g₂ a
⊢ Set.EqOn g₁ g₂ s

Tactic:
rw [← Set.restrict_eq_restrict_iff] at he ⊢

Result:
X : Type u_1
E : Type u_2
A : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace A
p : E → X
s : Set A
g₁ g₂ : A → E
sep : IsSeparatedMap p
inj : IsLocallyInjective p
hs : IsPreconnected s
h₁ : ContinuousOn g₁ s
h₂ : ContinuousOn g₂ s
he : s.restrict (p ∘ g₁) = s.restrict (p ∘ g₂)
a : A
has : a ∈ s
ha : g₁ a = g₂ a
⊢ s.restrict g₁ = s.restrict g₂

Proof state:
X : Type u_1
E : Type u_2
A : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace A
p : E → X
s : Set A
g₁ g₂ : A → E
sep : IsSeparatedMap p
inj : IsLocallyInjective p
hs : IsPreconnected s
h₁ : ContinuousOn g₁ s
h₂ : ContinuousOn g₂ s
he : s.restrict (p ∘ g₁) = s.restrict (p ∘ g₂)
a : A
has : a ∈ s
ha : g₁ a = g₂ a
⊢ s.restrict g₁ = s.restrict g₂

Tactic:
rw [continuousOn_iff_continuous_restrict] at h₁ h₂

Result:
X : Type u_1
E : Type u_2
A : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace A
p : E → X
s : Set A
g₁ g₂ : A → E
sep : IsSeparatedMap p
inj : IsLocallyInjective p
hs : IsPreconnected s
h₁ : Continuous (s.restrict g₁)
h₂ : Continuous (s.restrict g₂)
he : s.restrict (p ∘ g₁) = s.restrict (p ∘ g₂)
a : A
has : a ∈ s
ha : g₁ a = g₂ a
⊢ s.restrict g₁ = s.restrict g₂

Proof state:
X : Type u_1
E : Type u_2
A : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace A
p : E → X
s : Set A
g₁ g₂ : A → E
sep : IsSeparatedMap p
inj : IsLocallyInjective p
hs : IsPreconnected s
h₁ : Continuous (s.restrict g₁)
h₂ : Continuous (s.restrict g₂)
he : s.restrict (p ∘ g₁) = s.restrict (p ∘ g₂)
a : A
has : a ∈ s
ha : g₁ a = g₂ a
⊢ s.restrict g₁ = s.restrict g₂

Tactic:
rw [isPreconnected_iff_preconnectedSpace] at hs

Result:
X : Type u_1
E : Type u_2
A : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace A
p : E → X
s : Set A
g₁ g₂ : A → E
sep : IsSeparatedMap p
inj : IsLocallyInjective p
hs : PreconnectedSpace ↑s
h₁ : Continuous (s.restrict g₁)
h₂ : Continuous (s.restrict g₂)
he : s.restrict (p ∘ g₁) = s.restrict (p ∘ g₂)
a : A
has : a ∈ s
ha : g₁ a = g₂ a
⊢ s.restrict g₁ = s.restrict g₂

Proof state:
X : Type u_1
E : Type u_2
A : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace A
p : E → X
s : Set A
g₁ g₂ : A → E
sep : IsSeparatedMap p
inj : IsLocallyInjective p
hs : PreconnectedSpace ↑s
h₁ : Continuous (s.restrict g₁)
h₂ : Continuous (s.restrict g₂)
he : s.restrict (p ∘ g₁) = s.restrict (p ∘ g₂)
a : A
has : a ∈ s
ha : g₁ a = g₂ a
⊢ s.restrict g₁ = s.restrict g₂

Tactic:
exact sep.eq_of_comp_eq inj h₁ h₂ he ⟨a, has⟩ ha

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedLemmas.lean
theorem mkGateCached.go_eval_eq_mkGate_eval {aig : AIG α} {input : GateInput aig} :
    ⟦go aig input, assign⟧ = ⟦aig.mkGate input, assign⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
x✝⁴ : Option (CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv))
heq✝¹ : aig.cache.get? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = none
x✝³ x✝² : Decl α
linv✝ rinv✝ : Bool
heq : aig.decls[input.rhs.ref.gate] = Decl.const true
heq✝ : input.rhs.inv = true
x✝¹ : aig.decls[input.lhs.ref.gate] = Decl.const true → input.lhs.inv = true → False
x✝ : aig.decls[input.lhs.ref.gate] = Decl.const false → input.lhs.inv = false → False
⊢ ⟦assign, { decls := aig.decls, cache := aig.cache, invariant := ⋯ }.mkConstCached false⟧ = ⟦assign, aig.mkGate input⟧

Tactic:
simp_all [denote_idx_const heq]

Result:
no goals