harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Finiteness/Subalgebra.lean
theorem FG.mul (hm : M.FG) (hn : N.FG) : (M * N).FG

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
hm : M.FG
hn : N.FG
⊢ (Submodule.map₂ (LinearMap.mul R A) M N).FG

Tactic:
exact hm.map₂ _ hn

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
hm : M.FG
hn : N.FG
⊢ (M * N).FG

Tactic:
rw [mul_eq_map₂]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
hm : M.FG
hn : N.FG
⊢ (Submodule.map₂ (LinearMap.mul R A) M N).FG
-- Mathlib/Algebra/Lie/Derivation/Killing.lean
lemma killingForm_restrict_range_ad [Module.Finite R L] :
    (killingForm R 𝔻).restrict 𝕀 = killingForm R 𝕀

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : Field R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Module.Finite R L
⊢ (killingForm R (LieDerivation R L L)).restrict (ad R L).range.toSubmodule = killingForm R ↥(ad R L).range

Tactic:
rw [← (ad_isIdealMorphism R L).eq, ← LieIdeal.killingForm_eq]

Result:
R : Type u_1
L : Type u_2
inst✝³ : Field R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Module.Finite R L
⊢ killingForm R ↥(ad R L).idealRange =
    killingForm R ↥(LieIdeal.toLieSubalgebra R (LieDerivation R L L) (ad R L).idealRange)

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : Field R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Module.Finite R L
⊢ killingForm R ↥(ad R L).idealRange =
    killingForm R ↥(LieIdeal.toLieSubalgebra R (LieDerivation R L L) (ad R L).idealRange)

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem integrable_inv_smul_measure {f : α → β} {c : ℝ≥0∞} (h₁ : c ≠ 0) (h₂ : c ≠ ∞) :
    Integrable f (c⁻¹ • μ) ↔ Integrable f μ :=
  integrable_smul_measure (by simpa using h₂) (by simpa using h₁)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
c : ℝ≥0∞
h₁ : c ≠ 0
h₂ : c ≠ ⊤
⊢ c⁻¹ ≠ 0

Tactic:
simpa using h₂

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
c : ℝ≥0∞
h₁ : c ≠ 0
h₂ : c ≠ ⊤
⊢ c⁻¹ ≠ ⊤

Tactic:
simpa using h₁

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem ite_iff_left_iff {p : Prop} [Decidable p] {x y : Prop} : ((if p then x else y) ↔ x) ↔ ¬ p → y = x

Proof state:
p : Prop
inst✝ : Decidable p
x y : Prop
⊢ ((if p then x else y) ↔ x) ↔ ¬p → y = x

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem _root_.Polynomial.toLaurent_C_mul_eq (r : R) (f : R[X]) :
    toLaurent (Polynomial.C r * f) = C r * toLaurent f

Proof state:
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ toLaurent (Polynomial.C r * f) = C r * toLaurent f

Tactic:
simp only [_root_.map_mul, Polynomial.toLaurent_C]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem Lp.norm_constL_le (𝕜 : Type*) [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E]
    [Fact (1 ≤ p)] :
    ‖(Lp.constL p μ 𝕜 : E →L[𝕜] Lp E p μ)‖ ≤ (μ Set.univ).toReal ^ (1 / p.toReal) :=
  LinearMap.mkContinuous_norm_le _ (by positivity) _

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : IsFiniteMeasure μ
𝕜 : Type u_7
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Fact (1 ≤ p)
⊢ 0 ≤ (μ Set.univ).toReal ^ (1 / p.toReal)

Tactic:
positivity

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem deriv_div_const (d : 𝕜') : deriv (fun x => c x / d) x = deriv c x / d

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c : 𝕜 → 𝕜'
d : 𝕜'
⊢ deriv (fun x => c x / d) x = deriv c x / d

Tactic:
simp only [div_eq_mul_inv, deriv_mul_const_field]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/CommShift.lean
@[simp]
lemma isoAdd_hom_app {a b : A}
    (e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a)
    (e₂ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b) (X : C) :
      (CommShift.isoAdd e₁ e₂).hom.app X =
        F.map ((shiftFunctorAdd C a b).hom.app X) ≫ e₂.hom.app ((shiftFunctor C a).obj X) ≫
          (shiftFunctor D b).map (e₁.hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_7, u_1} C
inst✝³ : Category.{u_6, u_2} D
F : C ⥤ D
A : Type u_4
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
X : C
⊢ (isoAdd e₁ e₂).hom.app X =
    F.map ((shiftFunctorAdd C a b).hom.app X) ≫
      e₂.hom.app ((shiftFunctor C a).obj X) ≫
        (shiftFunctor D b).map (e₁.hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)

Tactic:
simp only [isoAdd, isoAdd'_hom_app, shiftFunctorAdd'_eq_shiftFunctorAdd]

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem conjugate {x : R} (hx : IsSelfAdjoint x) (z : R) : IsSelfAdjoint (z * x * star z)

Proof state:
R : Type u_1
inst✝¹ : Semigroup R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
z : R
⊢ IsSelfAdjoint (z * x * star z)

Tactic:
simp only [isSelfAdjoint_iff, star_mul, star_star, mul_assoc, hx.star_eq]

Result:
no goals
-- Mathlib/Data/Multiset/Count.lean
theorem card_eq_countP_add_countP (s) : card s = countP p s + countP (fun x => ¬p x) s :=
  Quot.inductionOn s fun l => by simp [l.length_eq_countP_add_countP p]

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ card (Quot.mk (⇑(isSetoid α)) l) =
    countP p (Quot.mk (⇑(isSetoid α)) l) + countP (fun x => ¬p x) (Quot.mk (⇑(isSetoid α)) l)

Tactic:
simp [l.length_eq_countP_add_countP p]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_modify [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : β → β} (h : m.WF) :
    (Const.modify m k f).getKeyD k' fallback =
      if k == k' then
        if k ∈ m then k else fallback
      else
        m.getKeyD k' fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' fallback : α
f : β → β
h : m.WF
⊢ (modify m k f).getKeyD k' fallback =
    if (k == k') = true then if m.contains k = true then k else fallback else m.getKeyD k' fallback

Tactic:
simp_to_raw using Raw₀.Const.getKeyD_modify

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' fallback : α
f : β → β
h : m.WF
⊢ (modify m k f).getKeyD k' fallback = if (k == k') = true then if k ∈ m then k else fallback else m.getKeyD k' fallback

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' fallback : α
f : β → β
h : m.WF
⊢ (modify m k f).getKeyD k' fallback =
    if (k == k') = true then if m.contains k = true then k else fallback else m.getKeyD k' fallback
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem descPochhammer_int_eq_ascFactorial (a b : ℕ) :
    (descPochhammer ℤ b).eval (a + b : ℤ) = (a + 1).ascFactorial b

Proof state:
a b : ℕ
⊢ eval (↑a + ↑b) (descPochhammer ℤ b) = ↑((a + 1).ascFactorial b)

Tactic:
rw [← Nat.cast_add, descPochhammer_eval_eq_descFactorial ℤ (a + b) b,
  Nat.add_descFactorial_eq_ascFactorial]

Result:
no goals
-- Mathlib/Algebra/Lie/UniversalEnveloping.lean
theorem lift_ι_apply' (x : L) :
    lift R f ((UniversalEnvelopingAlgebra.mkAlgHom R L) (ιₜ x)) = f x

Proof state:
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
x : L
⊢ ((lift R) f) ((mkAlgHom R L) (ιₜ x)) = f x

Tactic:
simpa using lift_ι_apply R f x

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem add_div_of_dvd_left {a b c : ℕ} (hca : c ∣ b) : (a + b) / c = a / c + b / c

Proof state:
a b c : ℕ
hca : c ∣ b
⊢ (a + b) / c = a / c + b / c

Tactic:
rwa [add_comm, Nat.add_div_of_dvd_right, add_comm]

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
lemma surjective_fromQuotient_iff_surjective_π :
    Function.Surjective solution.fromQuotient ↔ Function.Surjective solution.π

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ Function.Surjective ⇑solution.fromQuotient ↔ Function.Surjective ⇑solution.π

Tactic:
simpa only [← fromQuotient_comp_toQuotient] using
  (Function.Surjective.of_comp_iff (f := solution.fromQuotient)
    relations.surjective_toQuotient).symm

Result:
no goals
-- Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
lemma isIso_ranAdjunction_unit_app_iff (G : D ⥤ H) :
    IsIso ((L.ranAdjunction H).unit.app G) ↔ G.IsRightKanExtension (𝟙 (L ⋙ G)) :=
  (isRightKanExtension_iff_isIso _ (L.ranCounit.app (L ⋙ G)) _ (by simp)).symm

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{u_5, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
G : D ⥤ H
⊢ whiskerLeft L ((L.ranAdjunction H).unit.app G) ≫ L.ranCounit.app (L ⋙ G) = 𝟙 (L ⋙ G)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_cast {a : α} {l : Vector α n} {m : Nat} {w : n = m} :
    a ∈ l.cast w ↔ a ∈ l

Proof state:
α : Type u_1
n : Nat
a : α
l : Vector α n
m : Nat
w : n = m
⊢ a ∈ Vector.cast w l ↔ a ∈ l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
a : α
m : Nat
l : Array α
w : l.size = m
⊢ a ∈ Vector.cast w { toArray := l, size_toArray := ⋯ } ↔ a ∈ { toArray := l, size_toArray := ⋯ }

Proof state:
case mk
α : Type u_1
a : α
m : Nat
l : Array α
w : l.size = m
⊢ a ∈ Vector.cast w { toArray := l, size_toArray := ⋯ } ↔ a ∈ { toArray := l, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
theorem logEmbedding_fundSystem (i : Fin (rank K)) :
    logEmbedding K (Additive.ofMul (fundSystem K i)) = basisUnitLattice K i

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : Fin (rank K)
⊢ (logEmbedding K) (Additive.ofMul (fundSystem K i)) = ↑((basisUnitLattice K) i)

Tactic:
rw [basisUnitLattice, Basis.map_apply, ← fundSystem_mk, logEmbeddingEquiv_apply]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : Fin (rank K)
⊢ (logEmbedding K) (Additive.ofMul (fundSystem K i)) = ↑(sorry i)
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable
then for nonnegative `p : ℝ`, `|X| ^ p * exp (v * X)` is integrable. -/
lemma integrable_rpow_abs_mul_exp_of_integrable_exp_mul (ht : t ≠ 0)
    (ht_int_pos : Integrable (fun ω ↦ exp ((v + t) * X ω)) μ)
    (ht_int_neg : Integrable (fun ω ↦ exp ((v - t) * X ω)) μ) {p : ℝ} (hp : 0 ≤ p) :
    Integrable (fun ω ↦ |X ω| ^ p * exp (v * X ω)) μ

Proof state:
case h.e'_6.h.h.e'_6.h.e'_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
x✝ : Ω
⊢ v * X x✝ = v * X x✝ + 0 * |X x✝|

Tactic:
simp

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω => |X ω| ^ p * rexp (v * X ω)) μ

Tactic:
convert integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul ht_int_pos ht_int_neg le_rfl _ hp
  using 4

Result:
case h.e'_6.h.h.e'_6.h.e'_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
x✝ : Ω
⊢ v * X x✝ = v * X x✝ + 0 * |X x✝|

Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ 0 < |t|

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ 0 < |t|

Tactic:
simp [ht]

Result:
no goals
-- Mathlib/Order/Hom/Basic.lean
theorem map_inv_le_map_inv_iff (f : F) {a b : β} :
    EquivLike.inv f b ≤ EquivLike.inv f a ↔ b ≤ a

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LE α
inst✝² : LE β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a b : β
⊢ EquivLike.inv f b ≤ EquivLike.inv f a ↔ b ≤ a

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem simple_mul_simple_pow (i i' : B) : (s i * s i') ^ M i i' = 1

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
⊢ (cs.simple i * cs.simple i') ^ M.M i i' = 1

Tactic:
have : (FreeGroup.of i * FreeGroup.of i') ^ M i i' ∈ M.relationsSet := ⟨(i, i'), rfl⟩

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
this : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet
⊢ (cs.simple i * cs.simple i') ^ M.M i i' = 1

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
this✝ : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet
this : (PresentedGroup.mk M.relationsSet) ((FreeGroup.of i * FreeGroup.of i') ^ M.M i i') = 1
⊢ (cs.mulEquiv.symm (PresentedGroup.of i) * cs.mulEquiv.symm (PresentedGroup.of i')) ^ M.M i i' = 1

Tactic:
rw [← map_mul, ← map_pow]

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
this✝ : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet
this : (PresentedGroup.mk M.relationsSet) ((FreeGroup.of i * FreeGroup.of i') ^ M.M i i') = 1
⊢ cs.mulEquiv.symm ((PresentedGroup.of i * PresentedGroup.of i') ^ M.M i i') = 1

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
this✝ : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet
this : (PresentedGroup.mk M.relationsSet) ((FreeGroup.of i * FreeGroup.of i') ^ M.M i i') = 1
⊢ cs.mulEquiv.symm ((PresentedGroup.of i * PresentedGroup.of i') ^ M.M i i') = 1

Tactic:
exact (MulEquiv.map_eq_one_iff cs.mulEquiv.symm).mpr this

Result:
no goals

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
this : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet
⊢ (cs.simple i * cs.simple i') ^ M.M i i' = 1

Tactic:
have : (PresentedGroup.mk _ ((FreeGroup.of i * FreeGroup.of i') ^ M i i') : M.Group) = 1 :=
  (QuotientGroup.eq_one_iff _).mpr (Subgroup.subset_normalClosure this)

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
this✝ : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet
this : (PresentedGroup.mk M.relationsSet) ((FreeGroup.of i * FreeGroup.of i') ^ M.M i i') = 1
⊢ (cs.simple i * cs.simple i') ^ M.M i i' = 1

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
this✝ : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet
this : (PresentedGroup.mk M.relationsSet) ((FreeGroup.of i * FreeGroup.of i') ^ M.M i i') = 1
⊢ (cs.simple i * cs.simple i') ^ M.M i i' = 1

Tactic:
unfold simple

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
this✝ : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet
this : (PresentedGroup.mk M.relationsSet) ((FreeGroup.of i * FreeGroup.of i') ^ M.M i i') = 1
⊢ (cs.mulEquiv.symm (PresentedGroup.of i) * cs.mulEquiv.symm (PresentedGroup.of i')) ^ M.M i i' = 1
-- Mathlib/Logic/Relation.lean
@[simp] lemma reflTransGen_transGen : ReflTransGen (TransGen r) = ReflTransGen r

Proof state:
α : Type u_1
r : α → α → Prop
⊢ ReflTransGen (TransGen r) = ReflTransGen r

Tactic:
simp only [← reflGen_transGen, transGen_idem]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem sin_angle_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2)
    (h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂) : Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃

Tactic:
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃,
  add_comm, sin_angle_add_of_inner_eq_zero h h0]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂
⊢ Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃

Tactic:
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
  inner_neg_left, neg_vsub_eq_vsub_rev] at h

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂
⊢ Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂
⊢ Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃

Tactic:
rw [← @vsub_ne_zero V, @ne_comm _ p₃, ← @vsub_ne_zero V _ _ _ p₂, or_comm] at h0

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
-- Mathlib/SetTheory/Surreal/Basic.lean
theorem le_iff_forall_lt {x y : PGame} (ox : x.Numeric) (oy : y.Numeric) :
    x ≤ y ↔ (∀ i, x.moveLeft i < y) ∧ ∀ j, x < y.moveRight j

Proof state:
x y : PGame
ox : x.Numeric
oy : y.Numeric
⊢ x ≤ y ↔ (∀ (i : x.LeftMoves), x.moveLeft i < y) ∧ ∀ (j : y.RightMoves), x < y.moveRight j

Tactic:
refine le_iff_forall_lf.trans (and_congr ?_ ?_) <;>
    refine forall_congr' fun i => lf_iff_lt ?_ ?_ <;>
  apply_rules [Numeric.moveLeft, Numeric.moveRight]

Result:
no goals
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem eraseLead_monomial (i : ℕ) (r : R) : eraseLead (monomial i r) = 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
i : ℕ
r : R
hr : ¬r = 0
⊢ ((monomial i) r).eraseLead = 0

Tactic:
rw [eraseLead, natDegree_monomial, if_neg hr, erase_monomial]

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
i : ℕ
r : R
hr : r = 0
⊢ ((monomial i) r).eraseLead = 0

Tactic:
subst r

Result:
case pos
R : Type u_1
inst✝ : Semiring R
i : ℕ
⊢ ((monomial i) 0).eraseLead = 0

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
i : ℕ
⊢ ((monomial i) 0).eraseLead = 0

Tactic:
simp only [monomial_zero_right, eraseLead_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
i : ℕ
r : R
⊢ ((monomial i) r).eraseLead = 0

Tactic:
by_cases hr : r = 0

Result:
case pos
R : Type u_1
inst✝ : Semiring R
i : ℕ
r : R
hr : r = 0
⊢ ((monomial i) r).eraseLead = 0

case neg
R : Type u_1
inst✝ : Semiring R
i : ℕ
r : R
hr : ¬r = 0
⊢ ((monomial i) r).eraseLead = 0
-- Mathlib/Order/SupClosed.lean
@[simp] protected lemma LinearOrder.supClosed (s : Set α) : SupClosed s :=
  fun a ha b hb ↦ by cases le_total a b <;> simp [*]

Proof state:
α : Type u_3
inst✝ : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a ⊔ b ∈ s

Tactic:
cases le_total a b <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma rightUnshift_rightShift (a n' : ℤ) (hn' : n' + a = n) :
    (γ.rightShift a n' hn').rightUnshift n hn' = γ

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n = q
⊢ ((γ.rightShift a n' hn').rightUnshift n hn').v p q hpq = γ.v p q hpq

Tactic:
simp only [rightUnshift_v _ n hn' p q hpq (p + n') rfl,
  γ.rightShift_v _ _ hn' p (p + n') rfl q hpq,
  shiftFunctorObjXIso, assoc, Iso.inv_hom_id, comp_id]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
⊢ (γ.rightShift a n' hn').rightUnshift n hn' = γ

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n = q
⊢ ((γ.rightShift a n' hn').rightUnshift n hn').v p q hpq = γ.v p q hpq
-- Mathlib/RepresentationTheory/Rep.lean
theorem MonoidalClosed.linearHomEquiv_symm_hom (f : B ⟶ A ⟶[Rep k G] C) :
    ((MonoidalClosed.linearHomEquiv A B C).symm f).hom =
      ModuleCat.ofHom (TensorProduct.uncurry k A B C f.hom.hom.flip)

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B C : Rep k G
f : B ⟶ (ihom A).obj C
⊢ ((linearHomEquiv A B C).symm f).hom =
    ModuleCat.ofHom ((TensorProduct.uncurry k ↑A.V ↑B.V ↑C.V) (ModuleCat.Hom.hom f.hom).flip)

Tactic:
simp [linearHomEquiv]

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B C : Rep k G
f : B ⟶ (ihom A).obj C
⊢ ((A.homEquiv B C).symm f).hom =
    ModuleCat.ofHom ((TensorProduct.uncurry k ↑A.V ↑B.V ↑C.V) (ModuleCat.Hom.hom f.hom).flip)

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B C : Rep k G
f : B ⟶ (ihom A).obj C
⊢ ((A.homEquiv B C).symm f).hom =
    ModuleCat.ofHom ((TensorProduct.uncurry k ↑A.V ↑B.V ↑C.V) (ModuleCat.Hom.hom f.hom).flip)

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basis.lean
@[simp]
lemma TensorProduct.equivFinsuppOfBasisLeft_apply_tmul (m : M) (n : N) :
    (TensorProduct.equivFinsuppOfBasisLeft ℬ) (m ⊗ₜ n) =
    (ℬ.repr m).mapRange (· • n) (zero_smul _ _)

Proof state:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
ℬ : Basis ι R M
m : M
n : N
⊢ (equivFinsuppOfBasisLeft ℬ) (m ⊗ₜ[R] n) = Finsupp.mapRange (fun x => x • n) ⋯ (ℬ.repr m)

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
ℬ : Basis ι R M
m : M
n : N
a✝ : ι
⊢ ((equivFinsuppOfBasisLeft ℬ) (m ⊗ₜ[R] n)) a✝ = (Finsupp.mapRange (fun x => x • n) ⋯ (ℬ.repr m)) a✝

Proof state:
case h
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
ℬ : Basis ι R M
m : M
n : N
a✝ : ι
⊢ ((equivFinsuppOfBasisLeft ℬ) (m ⊗ₜ[R] n)) a✝ = (Finsupp.mapRange (fun x => x • n) ⋯ (ℬ.repr m)) a✝

Tactic:
simp [equivFinsuppOfBasisLeft]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_intCast_mul (hx : 0 ≤ x) (n : ℤ) (z : ℝ) : x ^ (n * z) = (x ^ n) ^ z

Proof state:
x : ℝ
hx : 0 ≤ x
n : ℤ
z : ℝ
⊢ x ^ (↑n * z) = (x ^ n) ^ z

Tactic:
rw [rpow_mul hx, rpow_intCast]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem eq_mul_of_mul_inv_eq (h : a * c⁻¹ = b) : a = b * c

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
h : a * c⁻¹ = b
⊢ a = b * c

Tactic:
simp [h.symm]

Result:
no goals