harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem IsIntegral.tmul (x : A) {y : B} (h : IsIntegral R y) : IsIntegral A (x ⊗ₜ[R] y)

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A
y : B
h : IsIntegral R y
⊢ IsIntegral A (x • 1 ⊗ₜ[R] y)

Tactic:
exact smul _ (h.map_of_comp_eq (algebraMap R A)
  (Algebra.TensorProduct.includeRight (R := R) (A := A) (B := B)).toRingHom
  Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap)

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A
y : B
h : IsIntegral R y
⊢ IsIntegral A (x ⊗ₜ[R] y)

Tactic:
rw [← mul_one x, ← smul_eq_mul, ← smul_tmul']

Result:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A
y : B
h : IsIntegral R y
⊢ IsIntegral A (x • 1 ⊗ₜ[R] y)
-- Mathlib/Topology/UniformSpace/Ascoli.lean
/-- Let `X` be a compact topological space, `α` a uniform space, and `F : ι → (X → α)` an
equicontinuous family. Then, the topologies of uniform convergence and pointwise convergence induce
the same topology on `ι`.

In other words, pointwise convergence and uniform convergence coincide on an equicontinuous
subset of `X → α`.

This is a consequence of `Equicontinuous.comap_uniformFun_eq`, stated in terms of `IsInducing`
for convenuence. -/
lemma Equicontinuous.inducing_uniformFun_iff_pi [TopologicalSpace ι] [CompactSpace X]
    (F_eqcont : Equicontinuous F) :
    IsInducing (UniformFun.ofFun ∘ F) ↔ IsInducing F

Proof state:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : TopologicalSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ inst✝¹ = TopologicalSpace.induced (⇑UniformFun.ofFun ∘ F) (UniformFun.topologicalSpace X α) ↔
    inst✝¹ = TopologicalSpace.induced F Pi.topologicalSpace

Tactic:
change (_ = (UniformFun.uniformSpace X α |>.comap F |>.toTopologicalSpace)) ↔
       (_ = (Pi.uniformSpace _ |>.comap F |>.toTopologicalSpace))

Result:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : TopologicalSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ inst✝¹ = UniformSpace.toTopologicalSpace ↔ inst✝¹ = UniformSpace.toTopologicalSpace

Proof state:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : TopologicalSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ IsInducing (⇑UniformFun.ofFun ∘ F) ↔ IsInducing F

Tactic:
rw [isInducing_iff, isInducing_iff]

Result:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : TopologicalSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ inst✝¹ = TopologicalSpace.induced (⇑UniformFun.ofFun ∘ F) (UniformFun.topologicalSpace X α) ↔
    inst✝¹ = TopologicalSpace.induced F Pi.topologicalSpace

Proof state:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : TopologicalSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ inst✝¹ = UniformSpace.toTopologicalSpace ↔ inst✝¹ = UniformSpace.toTopologicalSpace

Tactic:
rw [F_eqcont.comap_uniformFun_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem support_eq [MeasurableSpace α] [Zero β] (f : α →ₛ β) :
    support f = ⋃ y ∈ {y ∈ f.range | y ≠ 0}, f ⁻¹' {y} :=
  Set.ext fun x => by
    simp only [mem_support, Set.mem_preimage, mem_filter, mem_range_self, true_and, exists_prop,
      mem_iUnion, Set.mem_range, mem_singleton_iff, exists_eq_right']

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
f : α →ₛ β
x : α
⊢ x ∈ support ⇑f ↔ x ∈ ⋃ y ∈ filter (fun y => y ≠ 0) f.range, ⇑f ⁻¹' {y}

Tactic:
simp only [mem_support, Set.mem_preimage, mem_filter, mem_range_self, true_and, exists_prop,
  mem_iUnion, Set.mem_range, mem_singleton_iff, exists_eq_right']

Result:
no goals
-- Mathlib/Data/List/ReduceOption.lean
theorem reduceOption_singleton (x : Option α) : [x].reduceOption = x.toList

Proof state:
α : Type u_1
x : Option α
⊢ [x].reduceOption = x.toList

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Lemmas.lean
/-- There is always a character on `F` of order `#F-1` with values in a ring that has
a primitive `(#F-1)`th root of unity. -/
lemma exists_mulChar_orderOf_eq_card_units [DecidableEq F]
    {ζ : R} (hζ : IsPrimitiveRoot ζ (Fintype.card Fˣ)) :
    ∃ χ : MulChar F R, orderOf χ = Fintype.card Fˣ :=
  exists_mulChar_orderOf F (by rw [Fintype.card_units]) hζ

Proof state:
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : DecidableEq F
ζ : R
hζ : IsPrimitiveRoot ζ (Fintype.card Fˣ)
⊢ Fintype.card Fˣ ∣ Fintype.card F - 1

Tactic:
rw [Fintype.card_units]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem equicontinuous_finite [Finite ι] {F : ι → X → α} :
    Equicontinuous F ↔ ∀ i, Continuous (F i)

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
inst✝ : Finite ι
F : ι → X → α
⊢ Equicontinuous F ↔ ∀ (i : ι), Continuous (F i)

Tactic:
simp only [Equicontinuous, equicontinuousAt_finite, continuous_iff_continuousAt, @forall_swap ι]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
@[simp]
lemma smul_lt_iff_lt_one_left [SMulPosStrictMono α β] [SMulPosReflectLT α β] (hb : 0 < b) :
    a • b < b ↔ a < 1 := Iff.trans (by rw [one_smul]) (smul_lt_smul_iff_of_pos_right hb)

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Monoid α
inst✝⁵ : Zero β
inst✝⁴ : MulAction α β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : SMulPosStrictMono α β
inst✝ : SMulPosReflectLT α β
hb : 0 < b
⊢ a • b < b ↔ a • b < 1 • b

Tactic:
rw [one_smul]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Finset.lean
protected lemma sup_add (hs : s.Nonempty) (f : ι → M) (a : M) :
    s.sup f + a = s.sup fun i ↦ f i + a

Proof state:
ι : Type u_1
M : Type u_3
inst✝⁴ : LinearOrderedAddCommMonoid M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
hs : s.Nonempty
f : ι → M
a : M
⊢ s.sup f + a = s.sup fun i => f i + a

Tactic:
rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, sup'_add']

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc (attr := simp)]
lemma lift_snd {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) : lift f g ≫ snd _ _ = g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
T X Y : C
f : T ⟶ X
g : T ⟶ Y
⊢ lift f g ≫ snd X Y = g

Tactic:
simp [lift, snd]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_intCast {α : Type*} [LinearOrderedRing α] [FloorSemiring α] (z : ℤ) :
    ⌈(z : α)⌉₊ = z.toNat :=
  eq_of_forall_ge_iff fun a => by
    simp only [ceil_le, Int.toNat_le]
    norm_cast

Proof state:
α : Type u_4
inst✝¹ : LinearOrderedRing α
inst✝ : FloorSemiring α
z : ℤ
a : ℕ
⊢ ↑z ≤ ↑a ↔ z ≤ ↑a

Tactic:
norm_cast

Result:
no goals

Proof state:
α : Type u_4
inst✝¹ : LinearOrderedRing α
inst✝ : FloorSemiring α
z : ℤ
a : ℕ
⊢ ⌈↑z⌉₊ ≤ a ↔ z.toNat ≤ a

Tactic:
simp only [ceil_le, Int.toNat_le]

Result:
α : Type u_4
inst✝¹ : LinearOrderedRing α
inst✝ : FloorSemiring α
z : ℤ
a : ℕ
⊢ ↑z ≤ ↑a ↔ z ≤ ↑a
-- Mathlib/Order/BooleanAlgebra.lean
theorem inf_sdiff_distrib_left (a b c : α) : a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c)

Proof state:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c)

Tactic:
rw [sdiff_inf, sdiff_eq_bot_iff.2 inf_le_left, bot_sup_eq, inf_sdiff_assoc]

Result:
no goals
-- Mathlib/Data/Finsupp/NeLocus.lean
theorem neLocus_comm : f.neLocus g = g.neLocus f

Proof state:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
⊢ f.neLocus g = g.neLocus f

Tactic:
simp_rw [neLocus, Finset.union_comm, ne_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {v : β k} :
    (m.insertIfNew k v).getKey? a =
      if k == a ∧ m.contains k = false then some k else m.getKey? a

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a : α
v : β k
⊢ (m.insertIfNew k v).getKey? a = if (k == a) = true ∧ m.contains k = false then some k else m.getKey? a

Tactic:
simp_to_model [insertIfNew] using List.getKey?_insertEntryIfNew

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
/-- The iterated derivative commutes with shifting the function by a constant on the left. -/
lemma iteratedFDeriv_comp_add_left (n : ℕ) (a : E) (x : E) :
    iteratedFDeriv 𝕜 n (fun z ↦ f (a + z)) x = iteratedFDeriv 𝕜 n f (a + x)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
a x : E
⊢ iteratedFDeriv 𝕜 n (fun z => f (a + z)) x = iteratedFDeriv 𝕜 n f (a + x)

Tactic:
simp [iteratedFDeriv_comp_add_left']

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
@[simp]
lemma variableChange_j : (W.variableChange C).j = W.j

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst✝ : W.IsElliptic
⊢ (W.variableChange C).j = W.j

Tactic:
rw [j, coe_inv_variableChange_Δ', variableChange_c₄, j, mul_pow, ← pow_mul, ← mul_assoc,
  mul_right_comm (C.u.val ^ 12), ← mul_pow, C.u.mul_inv, one_pow, one_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Category.lean
theorem epi_of_epi_app (α : F ⟶ G) [∀ X : C, Epi (α.app X)] : Epi α :=
  ⟨fun g h eq => by
    ext X
    rw [← cancel_epi (α.app X), ← comp_app, eq, comp_app]⟩

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
inst✝ : ∀ (X : C), Epi (α.app X)
Z✝ : C ⥤ D
g h : G ⟶ Z✝
eq : α ≫ g = α ≫ h
⊢ g = h

Tactic:
ext X

Result:
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
inst✝ : ∀ (X : C), Epi (α.app X)
Z✝ : C ⥤ D
g h : G ⟶ Z✝
eq : α ≫ g = α ≫ h
X : C
⊢ g.app X = h.app X

Proof state:
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
inst✝ : ∀ (X : C), Epi (α.app X)
Z✝ : C ⥤ D
g h : G ⟶ Z✝
eq : α ≫ g = α ≫ h
X : C
⊢ g.app X = h.app X

Tactic:
rw [← cancel_epi (α.app X), ← comp_app, eq, comp_app]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Ico_add_one_right_eq_Icc_of_not_isMax (hb : ¬ IsMax b) (a : α) : Ico a (b + 1) = Icc a b

Proof state:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ico a (b + 1) = Icc a b

Tactic:
simpa [succ_eq_add_one] using Ico_succ_right_eq_Icc_of_not_isMax hb a

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem inter_biInter {ι α : Type*} {s : Set ι} (hs : s.Nonempty) (f : ι → Set α) (t : Set α) :
    ⋂ i ∈ s, t ∩ f i = t ∩ ⋂ i ∈ s, f i

Proof state:
ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
⊢ ⋂ i ∈ s, t ∩ f i = t ∩ ⋂ i ∈ s, f i

Tactic:
rw [inter_comm, ← biInter_inter hs]

Result:
ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
⊢ ⋂ i ∈ s, t ∩ f i = ⋂ i ∈ s, f i ∩ t

Proof state:
ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
⊢ ⋂ i ∈ s, t ∩ f i = ⋂ i ∈ s, f i ∩ t

Tactic:
simp [inter_comm]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem aleph0_le_mul_iff {a b : Cardinal} : ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)

Proof state:
a b : Cardinal.{u_1}
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)

Tactic:
let h := (@mul_lt_aleph0_iff a b).not

Result:
a b : Cardinal.{u_1}
h : ¬a * b < ℵ₀ ↔ ¬(a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀) := Iff.not mul_lt_aleph0_iff
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)

Proof state:
a b : Cardinal.{u_1}
h : ¬a * b < ℵ₀ ↔ ¬(a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀) := Iff.not mul_lt_aleph0_iff
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)

Tactic:
rwa [not_lt, not_or, not_or, not_and_or, not_lt, not_lt] at h

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
/-- The iterated derivative commutes with shifting the function by a constant on the right. -/
lemma iteratedFDerivWithin_comp_add_right' (n : ℕ) (a : E) :
    iteratedFDerivWithin 𝕜 n (fun z ↦ f (z + a)) s =
      fun x ↦ iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ
a : E
⊢ iteratedFDerivWithin 𝕜 n (fun z => f (z + a)) s = fun x => iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a)

Tactic:
simpa [add_comm a] using iteratedFDerivWithin_comp_add_left' n a

Result:
no goals
-- Mathlib/Algebra/Group/Even.lean
@[to_additive Even.zsmul_right] lemma IsSquare.zpow (n : ℤ) : IsSquare a → IsSquare (a ^ n)

Proof state:
α : Type u_2
inst✝ : DivisionMonoid α
a : α
n : ℤ
⊢ IsSquare a → IsSquare (a ^ n)

Tactic:
rintro ⟨r, rfl⟩

Result:
case intro
α : Type u_2
inst✝ : DivisionMonoid α
n : ℤ
r : α
⊢ IsSquare ((r * r) ^ n)

Proof state:
case intro
α : Type u_2
inst✝ : DivisionMonoid α
n : ℤ
r : α
⊢ IsSquare ((r * r) ^ n)

Tactic:
exact ⟨r ^ n, (Commute.refl _).mul_zpow _⟩

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Basic.lean
theorem tsub_add_min : a - b + min a b = a

Proof state:
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a - b + a ⊓ b = a

Tactic:
rw [← tsub_min, @tsub_add_cancel_of_le]

Result:
case h
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a ⊓ b ≤ a

Proof state:
case h
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a ⊓ b ≤ a

Tactic:
apply min_le_left

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem thickening_ball (hε : 0 < ε) (hδ : 0 < δ) (x : E) :
    thickening ε (ball x δ) = ball x (ε + δ)

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
x : E
⊢ thickening ε (Metric.ball x δ) = Metric.ball x (ε + δ)

Tactic:
rw [← thickening_singleton, thickening_thickening hε hδ, thickening_singleton]

Result:
no goals
-- Mathlib/Data/List/Zip.lean
theorem revzip_swap (l : List α) : (revzip l).map Prod.swap = revzip l.reverse

Proof state:
α : Type u
l : List α
⊢ map Prod.swap l.revzip = l.reverse.revzip

Tactic:
simp [revzip]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/OfFn.lean
theorem ofFn_zero (f : Fin 0 → α) : ofFn f = [] :=
  ext_get (by simp) (fun i hi₁ hi₂ => by contradiction)

Proof state:
α : Type u_1
f : Fin 0 → α
⊢ (ofFn f).length = [].length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
f : Fin 0 → α
i : Nat
hi₁ : i < (ofFn f).length
hi₂ : i < [].length
⊢ (ofFn f).get ⟨i, hi₁⟩ = [].get ⟨i, hi₂⟩

Tactic:
contradiction

Result:
no goals
-- Mathlib/GroupTheory/Submonoid/Inverses.lean
theorem leftInvEquiv_mul (x : S.leftInv) : (S.leftInvEquiv hS x : M) * x = 1

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S.leftInv
⊢ ↑((S.leftInvEquiv hS) x) * ↑x = 1

Tactic:
simpa only [leftInvEquiv_apply, fromCommLeftInv] using fromLeftInv_mul S x

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Cartan.lean
theorem rootSpaceProduct_tmul
    (χ₁ χ₂ χ₃ : H → R) (hχ : χ₁ + χ₂ = χ₃) (x : rootSpace H χ₁) (y : rootSpace H χ₂) :
    (rootSpaceProduct R L H χ₁ χ₂ χ₃ hχ (x ⊗ₜ y) : L) = ⁅(x : L), (y : L)⁆

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
χ₁ χ₂ χ₃ : ↥H → R
hχ : χ₁ + χ₂ = χ₃
x : ↥(rootSpace H χ₁)
y : ↥(rootSpace H χ₂)
⊢ ↑((rootSpaceProduct R L H χ₁ χ₂ χ₃ hχ) (x ⊗ₜ[R] y)) = ⁅↑x, ↑y⁆

Tactic:
simp only [rootSpaceProduct_def, coe_rootSpaceWeightSpaceProduct_tmul]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ToNat.lean
theorem mk_toNat_eq_card [Fintype α] : toNat #α = Fintype.card α

Proof state:
α : Type u
inst✝ : Fintype α
⊢ toNat #α = Fintype.card α

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem pow_eq_on_of_mem_support (h : ∀ x ∈ f.support ∩ g.support, f x = g x) (k : ℕ) :
    ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
k : ℕ
⊢ ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x

Tactic:
induction' k with k hk

Result:
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
⊢ ∀ x ∈ f.support ∩ g.support, (f ^ 0) x = (g ^ 0) x

case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x
⊢ ∀ x ∈ f.support ∩ g.support, (f ^ (k + 1)) x = (g ^ (k + 1)) x

Proof state:
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x
x : α
hx : x ∈ f.support ∩ g.support
⊢ (f ^ (k + 1)) x = (g ^ (k + 1)) x

Tactic:
rw [pow_succ, mul_apply, pow_succ, mul_apply, h _ hx, hk]

Result:
case succ.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x
x : α
hx : x ∈ f.support ∩ g.support
⊢ g x ∈ f.support ∩ g.support

Proof state:
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
⊢ ∀ x ∈ f.support ∩ g.support, (f ^ 0) x = (g ^ 0) x

Tactic:
simp

Result:
no goals

Proof state:
case succ.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x
x : α
hx : x ∈ f.support ∩ g.support
⊢ g x ∈ f.support ∩ g.support

Tactic:
rwa [mem_inter, apply_mem_support, ← h _ hx, apply_mem_support, ← mem_inter]

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x
⊢ ∀ x ∈ f.support ∩ g.support, (f ^ (k + 1)) x = (g ^ (k + 1)) x

Tactic:
intro x hx

Result:
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x
x : α
hx : x ∈ f.support ∩ g.support
⊢ (f ^ (k + 1)) x = (g ^ (k + 1)) x
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_one_le : cos 1 ≤ 2 / 3 :=
  calc
    cos 1 ≤ |(1 : ℝ)| ^ 4 * (5 / 96) + (1 - 1 ^ 2 / 2) :=
      sub_le_iff_le_add.1 (abs_sub_le_iff.1 (cos_bound (by simp))).1
    _ ≤ 2 / 3

Proof state:
⊢ |1| ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
⊢ |1| ^ 4 * (5 / 96) + (1 - 1 ^ 2 / 2) ≤ 2 / 3

Tactic:
norm_num

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_add_of_lt {n : ℕ} {a b : ZMod n} (h : a.val + b.val < n) :
    (a + b).val = a.val + b.val

Proof state:
n : ℕ
a b : ZMod n
h : a.val + b.val < n
⊢ (a + b).val = a.val + b.val

Tactic:
have : NeZero n := by constructor; rintro rfl; simp at h

Result:
n : ℕ
a b : ZMod n
h : a.val + b.val < n
this : NeZero n
⊢ (a + b).val = a.val + b.val

Proof state:
case out
a b : ZMod 0
h : a.val + b.val < 0
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
n : ℕ
a b : ZMod n
h : a.val + b.val < n
⊢ NeZero n

Tactic:
constructor

Result:
case out
n : ℕ
a b : ZMod n
h : a.val + b.val < n
⊢ n ≠ 0

Proof state:
case out
n : ℕ
a b : ZMod n
h : a.val + b.val < n
⊢ n ≠ 0

Tactic:
rintro rfl

Result:
case out
a b : ZMod 0
h : a.val + b.val < 0
⊢ False

Proof state:
n : ℕ
a b : ZMod n
h : a.val + b.val < n
this : NeZero n
⊢ (a + b).val = a.val + b.val

Tactic:
rw [ZMod.val_add, Nat.mod_eq_of_lt h]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.eq_iInf (h : l.HasBasis (fun _ => True) s) : l = ⨅ i, 𝓟 (s i)

Proof state:
α : Type u_1
ι : Sort u_4
l : Filter α
s : ι → Set α
h : l.HasBasis (fun x => True) s
⊢ l = ⨅ i, 𝓟 (s i)

Tactic:
simpa only [iInf_true] using h.eq_biInf

Result:
no goals
-- Mathlib/Data/List/Flatten.lean
theorem append_flatten_map_append (L : List (List α)) (x : List α) :
    x ++ (L.map (· ++ x)).flatten = (L.map (x ++ ·)).flatten ++ x

Proof state:
α : Type u_1
L : List (List α)
x : List α
⊢ x ++ (map (fun x_1 => x_1 ++ x) L).flatten = (map (fun x_1 => x ++ x_1) L).flatten ++ x

Tactic:
induction L with
| nil => rw [map_nil, flatten, append_nil, map_nil, flatten, nil_append]
| cons _ _ ih =>
  rw [map_cons, flatten, map_cons, flatten, append_assoc, ih, append_assoc, append_assoc]

Result:
no goals

Proof state:
case nil
α : Type u_1
x : List α
⊢ x ++ (map (fun x_1 => x_1 ++ x) []).flatten = (map (fun x_1 => x ++ x_1) []).flatten ++ x

Tactic:
rw [map_nil, flatten, append_nil, map_nil, flatten, nil_append]

Result:
no goals

Proof state:
case cons
α : Type u_1
x head✝ : List α
tail✝ : List (List α)
ih : x ++ (map (fun x_1 => x_1 ++ x) tail✝).flatten = (map (fun x_1 => x ++ x_1) tail✝).flatten ++ x
⊢ x ++ (map (fun x_1 => x_1 ++ x) (head✝ :: tail✝)).flatten = (map (fun x_1 => x ++ x_1) (head✝ :: tail✝)).flatten ++ x

Tactic:
rw [map_cons, flatten, map_cons, flatten, append_assoc, ih, append_assoc, append_assoc]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Bivariate.lean
lemma evalEval_list_prod (x y : R) (l : List R[X][Y]) :
    l.prod.evalEval x y = (l.map <| evalEval x y).prod

Proof state:
R : Type u_1
inst✝ : CommSemiring R
x y : R
l : List R[X][Y]
⊢ evalEval x y l.prod = (List.map (evalEval x y) l).prod

Tactic:
simpa only [evalEval, eval_list_prod, List.map_map] using by rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
x y : R
l : List R[X][Y]
⊢ (List.map (eval x ∘ eval (C y)) l).prod = (List.map (evalEval x y) l).prod

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem cos_add (θ₁ θ₂ : Real.Angle) : cos (θ₁ + θ₂) = cos θ₁ * cos θ₂ - sin θ₁ * sin θ₂

Proof state:
θ₁ θ₂ : Angle
⊢ (θ₁ + θ₂).cos = θ₁.cos * θ₂.cos - θ₁.sin * θ₂.sin

Tactic:
induction θ₂ using Real.Angle.induction_on

Result:
case h
θ₁ : Angle
x✝ : ℝ
⊢ (θ₁ + ↑x✝).cos = θ₁.cos * (↑x✝).cos - θ₁.sin * (↑x✝).sin

Proof state:
case h.h
x✝¹ x✝ : ℝ
⊢ (↑x✝ + ↑x✝¹).cos = (↑x✝).cos * (↑x✝¹).cos - (↑x✝).sin * (↑x✝¹).sin

Tactic:
exact Real.cos_add _ _

Result:
no goals

Proof state:
case h
θ₁ : Angle
x✝ : ℝ
⊢ (θ₁ + ↑x✝).cos = θ₁.cos * (↑x✝).cos - θ₁.sin * (↑x✝).sin

Tactic:
induction θ₁ using Real.Angle.induction_on

Result:
case h.h
x✝¹ x✝ : ℝ
⊢ (↑x✝ + ↑x✝¹).cos = (↑x✝).cos * (↑x✝¹).cos - (↑x✝).sin * (↑x✝¹).sin
-- Mathlib/ModelTheory/LanguageMap.lean
theorem withConstants_funMap_sumInr {a : α} {x : Fin 0 → M} :
    @funMap (L[[α]]) M _ 0 (Sum.inr a : L[[α]].Functions 0) x = L.con a

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u_1
inst✝ : (constantsOn α).Structure M
a : α
x : Fin 0 → M
⊢ funMap (Sum.inr a) x = ↑(L.con a)

Tactic:
rw [Unique.eq_default x]

Result:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u_1
inst✝ : (constantsOn α).Structure M
a : α
x : Fin 0 → M
⊢ funMap (Sum.inr a) default = ↑(L.con a)

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u_1
inst✝ : (constantsOn α).Structure M
a : α
x : Fin 0 → M
⊢ funMap (Sum.inr a) default = ↑(L.con a)

Tactic:
exact (LHom.sumInr : constantsOn α →ᴸ L.sum _).map_onFunction _ _

Result:
no goals