harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/VectorField.lean
theorem lieBracketWithin_congr_set' (y : E) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :
    lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W t x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s t : Set E
x y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W t x

Tactic:
simp [lieBracketWithin, fderivWithin_congr_set' _ h]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Basic.lean
theorem union_inter_cancel_right {s t : Finset α} : (s ∪ t) ∩ t = t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ (s ∪ t) ∩ t = t

Tactic:
rw [← coe_inj, coe_inter, coe_union, Set.union_inter_cancel_right]

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem unitGroup_injective : Function.Injective (unitGroup : ValuationSubring K → Subgroup _) :=
  fun A B h => by simpa only [le_antisymm_iff, unitGroup_le_unitGroup] using h

Proof state:
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup = B.unitGroup
⊢ A = B

Tactic:
simpa only [le_antisymm_iff, unitGroup_le_unitGroup] using h

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
@[reassoc (attr := simp)]
lemma stalkMap_inv_hom (e : X ≅ Y) (x : X) :
    e.inv.stalkMap (e.hom.base x) ≫ e.hom.stalkMap x =
      (X.presheaf.stalkCongr (.of_eq (by simp))).hom :=
  LocallyRingedSpace.stalkMap_inv_hom (forgetToLocallyRingedSpace.mapIso e) x

Proof state:
X Y : Scheme
f : X ⟶ Y
e : X ≅ Y
x : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom e.inv.base) ((ConcreteCategory.hom e.hom.base) x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem find?_some_mem {t : RBNode α} : x ∈ t.find? cut → x ∈ t

Proof state:
α : Type u_1
cut : α → Ordering
x : α
t : RBNode α
⊢ x ∈ find? cut t → x ∈ t

Tactic:
induction t <;> simp [find?]

Result:
case node
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : x ∈ find? cut l✝ → x ∈ l✝
r_ih✝ : x ∈ find? cut r✝ → x ∈ r✝
⊢ (match cut v✝ with
      | Ordering.lt => find? cut l✝
      | Ordering.gt => find? cut r✝
      | Ordering.eq => some v✝) =
      some x →
    x = v✝ ∨ x ∈ l✝ ∨ x ∈ r✝

Proof state:
case node
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : x ∈ find? cut l✝ → x ∈ l✝
r_ih✝ : x ∈ find? cut r✝ → x ∈ r✝
⊢ (match cut v✝ with
      | Ordering.lt => find? cut l✝
      | Ordering.gt => find? cut r✝
      | Ordering.eq => some v✝) =
      some x →
    x = v✝ ∨ x ∈ l✝ ∨ x ∈ r✝

Tactic:
split <;> simp (config := {contextual := true}) [*]

Result:
no goals
-- Mathlib/Tactic/CancelDenoms/Core.lean
theorem pow_subst {α} [CommRing α] {n e1 t1 k l : α} {e2 : ℕ}
    (h1 : n * e1 = t1) (h2 : l * n ^ e2 = k) : k * (e1 ^ e2) = l * t1 ^ e2

Proof state:
α : Type u_1
inst✝ : CommRing α
n e1 t1 k l : α
e2 : ℕ
h1 : n * e1 = t1
h2 : l * n ^ e2 = k
⊢ k * e1 ^ e2 = l * t1 ^ e2

Tactic:
rw [← h2, ← h1, mul_pow, mul_assoc]

Result:
no goals
-- Mathlib/InformationTheory/Hamming.lean
theorem hammingDist_comm (x y : ∀ i, β i) : hammingDist x y = hammingDist y x

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ hammingDist x y = hammingDist y x

Tactic:
simp_rw [hammingDist, ne_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/SeparableMeasure.lean
theorem measureDense_measurableSet : μ.MeasureDense {s | MeasurableSet s} where
  measurable _ h := h
  approx s hs _ ε ε_pos := ⟨s, hs, by simpa⟩

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
s : Set X
hs : MeasurableSet s
x✝ : μ s ≠ ⊤
ε : ℝ
ε_pos : 0 < ε
⊢ μ (s ∆ s) < ENNReal.ofReal ε

Tactic:
simpa

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
theorem map_add₂ (f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (x x' : M) (y : F) :
    f (x + x') y = f x y + f x' y

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹¹ : SeminormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
R : Type u_5
𝕜₂ : Type u_6
𝕜' : Type u_7
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NontriviallyNormedField 𝕜₂
M : Type u_8
inst✝⁷ : TopologicalSpace M
σ₁₂ : 𝕜 →+* 𝕜₂
G' : Type u_9
inst✝⁶ : SeminormedAddCommGroup G'
inst✝⁵ : NormedSpace 𝕜₂ G'
inst✝⁴ : NormedSpace 𝕜' G'
inst✝³ : SMulCommClass 𝕜₂ 𝕜' G'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ρ₁₂ : R →+* 𝕜'
f : M →SL[ρ₁₂] F →SL[σ₁₂] G'
x x' : M
y : F
⊢ (f (x + x')) y = (f x) y + (f x') y

Tactic:
rw [f.map_add, add_apply]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma map_φ (n : ℤ) : (W.map f).φ n = (W.φ n).map (mapRingHom f)

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (W.map f).φ n = Polynomial.map (mapRingHom f) (W.φ n)

Tactic:
simp only [φ, map_ψ]

Result:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ C X * Polynomial.map (mapRingHom f) (W.ψ n) ^ 2 -
      Polynomial.map (mapRingHom f) (W.ψ (n + 1)) * Polynomial.map (mapRingHom f) (W.ψ (n - 1)) =
    Polynomial.map (mapRingHom f) (C X * W.ψ n ^ 2 - W.ψ (n + 1) * W.ψ (n - 1))

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ C X * Polynomial.map (mapRingHom f) (W.ψ n) ^ 2 -
      Polynomial.map (mapRingHom f) (W.ψ (n + 1)) * Polynomial.map (mapRingHom f) (W.ψ (n - 1)) =
    Polynomial.map (mapRingHom f) (C X * W.ψ n ^ 2 - W.ψ (n + 1) * W.ψ (n - 1))

Tactic:
map_simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Poly.denote_combine (ctx : Context) (p₁ p₂ : Poly) : (p₁.combine p₂).denote ctx = p₁.denote ctx + p₂.denote ctx

Proof state:
ctx : Context
p₁ p₂ : Poly
⊢ denote ctx (p₁.combine p₂) = denote ctx p₁ + denote ctx p₂

Tactic:
simp [combine, denote_combineAux]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Bootstrap.lean
theorem push_toList (arr : Array α) (a : α) : (arr.push a).toList = arr.toList ++ [a]

Proof state:
α : Type u_1
arr : Array α
a : α
⊢ (arr.push a).toList = arr.toList ++ [a]

Tactic:
simp [push, List.concat_eq_append]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Basic.lean
theorem right_triangle : whiskerLeft G adj.unit ≫ whiskerRight adj.counit G = 𝟙 _

Proof state:
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝ : D
⊢ (whiskerLeft G adj.unit ≫ whiskerRight adj.counit G).app x✝ = (𝟙 (G ⋙ 𝟭 C)).app x✝

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
⊢ whiskerLeft G adj.unit ≫ whiskerRight adj.counit G = 𝟙 (G ⋙ 𝟭 C)

Tactic:
ext

Result:
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝ : D
⊢ (whiskerLeft G adj.unit ≫ whiskerRight adj.counit G).app x✝ = (𝟙 (G ⋙ 𝟭 C)).app x✝
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_mul' (x) {y : ℝ} (hy : 0 ≤ y) : √(x * y) = √x * √y

Proof state:
x y : ℝ
hy : 0 ≤ y
⊢ √(x * y) = √x * √y

Tactic:
rw [mul_comm, sqrt_mul hy, mul_comm]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sign_sub_left_swap (x y : V) : (o.oangle (x - y) x).sign = (o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ (o.oangle (x - y) x).sign = (o.oangle x y).sign

Tactic:
rw [oangle_sign_sub_left_eq_neg, o.oangle_rev y x, Real.Angle.sign_neg]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem zero_le_lf {x : PGame} : 0 ≤ x ↔ ∀ j, 0 ⧏ x.moveRight j

Proof state:
x : PGame
⊢ 0 ≤ x ↔ ∀ (j : x.RightMoves), 0 ⧏ x.moveRight j

Tactic:
rw [le_iff_forall_lf]

Result:
x : PGame
⊢ ((∀ (i : LeftMoves 0), moveLeft 0 i ⧏ x) ∧ ∀ (j : x.RightMoves), 0 ⧏ x.moveRight j) ↔
    ∀ (j : x.RightMoves), 0 ⧏ x.moveRight j

Proof state:
x : PGame
⊢ ((∀ (i : LeftMoves 0), moveLeft 0 i ⧏ x) ∧ ∀ (j : x.RightMoves), 0 ⧏ x.moveRight j) ↔
    ∀ (j : x.RightMoves), 0 ⧏ x.moveRight j

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_alter_of_beq_eq_false [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)}
    (h : m.WF) (he : (k == k') = false) : (m.alter k f).contains k' = m.contains k'

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
h : m.WF
he : (k == k') = false
⊢ (m.alter k f).contains k' = m.contains k'

Tactic:
simp only [contains_alter h, he, Bool.false_eq_true, reduceIte]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
@[to_additive (attr := simp)]
lemma coe_set_pow [SetLike S M] [SubmonoidClass S M] :
    ∀ {n} (hn : n ≠ 0) (H : S), (H ^ n : Set M) = H
  | 1, _, H => by simp
  | n + 2, _, H => by rw [pow_succ, coe_set_pow n.succ_ne_zero, coe_mul_coe]

Proof state:
M : Type u_3
S : Type u_6
inst✝² : Monoid M
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
n : ℕ
x✝ : n + 2 ≠ 0
H : S
⊢ ↑H ^ (n + 2) = ↑H

Tactic:
rw [pow_succ, coe_set_pow n.succ_ne_zero, coe_mul_coe]

Result:
no goals

Proof state:
M : Type u_3
S : Type u_6
inst✝² : Monoid M
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
x✝ : 1 ≠ 0
H : S
⊢ ↑H ^ 1 = ↑H

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem LipschitzOnWith.norm_div_le_of_le {f : E → F} {C : ℝ≥0} (h : LipschitzOnWith C f s)
    (ha : a ∈ s) (hb : b ∈ s) (hr : ‖a / b‖ ≤ r) : ‖f a / f b‖ ≤ C * r :=
  (h.norm_div_le ha hb).trans <| by gcongr

Proof state:
E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
s : Set E
a b : E
r : ℝ
f : E → F
C : ℝ≥0
h : LipschitzOnWith C f s
ha : a ∈ s
hb : b ∈ s
hr : ‖a / b‖ ≤ r
⊢ ↑C * ‖a / b‖ ≤ ↑C * r

Tactic:
gcongr

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Basic.lean
theorem lex_inr_inr : Lex r s (inr b₁) (inr b₂) ↔ s b₁ b₂ :=
  ⟨fun h => by cases h; assumption, Lex.inr⟩

Proof state:
case inr
α✝ : Type u_1
r : α✝ → α✝ → Prop
β✝ : Type u_2
s : β✝ → β✝ → Prop
b₁ b₂ : β✝
h✝ : s b₁ b₂
⊢ s b₁ b₂

Tactic:
assumption

Result:
no goals

Proof state:
α✝ : Type u_1
r : α✝ → α✝ → Prop
β✝ : Type u_2
s : β✝ → β✝ → Prop
b₁ b₂ : β✝
h : Lex r s (inr b₁) (inr b₂)
⊢ s b₁ b₂

Tactic:
cases h

Result:
case inr
α✝ : Type u_1
r : α✝ → α✝ → Prop
β✝ : Type u_2
s : β✝ → β✝ → Prop
b₁ b₂ : β✝
h✝ : s b₁ b₂
⊢ s b₁ b₂
-- Mathlib/Probability/Martingale/Basic.lean
theorem add (hf : Martingale f ℱ μ) (hg : Martingale g ℱ μ) : Martingale (f + g) ℱ μ

Proof state:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ι → Ω → E
ℱ : Filtration ι m0
hf : Martingale f ℱ μ
hg : Martingale g ℱ μ
⊢ Martingale (f + g) ℱ μ

Tactic:
refine ⟨hf.adapted.add hg.adapted, fun i j hij => ?_⟩

Result:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ι → Ω → E
ℱ : Filtration ι m0
hf : Martingale f ℱ μ
hg : Martingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ μ[(f + g) j|↑ℱ i] =ᶠ[ae μ] (f + g) i

Proof state:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ι → Ω → E
ℱ : Filtration ι m0
hf : Martingale f ℱ μ
hg : Martingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ μ[(f + g) j|↑ℱ i] =ᶠ[ae μ] (f + g) i

Tactic:
exact (condExp_add (hf.integrable j) (hg.integrable j) _).trans
  ((hf.2 i j hij).add (hg.2 i j hij))

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_union_Ioc_symm : Ioc a b ∪ Ioc b a = Ioc (min a b) (max a b)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioc a b ∪ Ioc b a = Ioc (a ⊓ b) (b ⊔ a)

Tactic:
apply Ioc_union_Ioc <;> rw [max_comm] <;> exact min_le_max

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioc a b ∪ Ioc b a = Ioc (a ⊓ b) (a ⊔ b)

Tactic:
rw [max_comm]

Result:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioc a b ∪ Ioc b a = Ioc (a ⊓ b) (b ⊔ a)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_abs {i : Nat} {x : BitVec w} :
    getLsbD x.abs i = if x.msb then getLsbD (-x) i else getLsbD x i

Proof state:
w i : Nat
x : BitVec w
⊢ x.abs.getLsbD i = if x.msb = true then (-x).getLsbD i else x.getLsbD i

Tactic:
by_cases h : x.msb <;> simp [BitVec.abs, h]

Result:
no goals
-- Mathlib/GroupTheory/Coprod/Basic.lean
theorem mrange_inl_sup_mrange_inr :
    MonoidHom.mrange (inl : M →* M ∗ N) ⊔ MonoidHom.mrange (inr : N →* M ∗ N) = ⊤

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ MonoidHom.mrange inl ⊔ MonoidHom.mrange inr = ⊤

Tactic:
rw [← mclosure_range_inl_union_inr, Submonoid.closure_union, ← MonoidHom.coe_mrange,
  ← MonoidHom.coe_mrange, Submonoid.closure_eq, Submonoid.closure_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
theorem _root_.Matrix.nondegenerate_toBilin_iff {M : Matrix ι ι R₂} (b : Basis ι R₂ M₂) :
    (Matrix.toBilin b M).Nondegenerate ↔ M.Nondegenerate

Proof state:
R₂ : Type u_3
M₂ : Type u_4
inst✝⁴ : CommRing R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
ι : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
M : Matrix ι ι R₂
b : Basis ι R₂ M₂
⊢ ((toBilin b) M).Nondegenerate ↔ M.Nondegenerate

Tactic:
rw [← Matrix.nondegenerate_toBilin'_iff_nondegenerate_toBilin, Matrix.nondegenerate_toBilin'_iff]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem X_pow_sub_one_splits {ζ : K} {n : ℕ} (h : IsPrimitiveRoot ζ n) :
    Splits (RingHom.id K) (X ^ n - C (1 : K))

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ Splits (RingHom.id K) (X ^ n - C 1)

Tactic:
rw [splits_iff_card_roots, ← nthRoots, IsPrimitiveRoot.card_nthRoots_one h, natDegree_X_pow_sub_C]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffEdist_zero_iff_closure_eq_closure :
    hausdorffEdist s t = 0 ↔ closure s = closure t

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEdist s t = 0 ↔ closure s = closure t

Tactic:
simp only [hausdorffEdist_def, ENNReal.sup_eq_zero, ENNReal.iSup_eq_zero, ← subset_def,
  ← mem_closure_iff_infEdist_zero, subset_antisymm_iff, isClosed_closure.closure_subset_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
theorem midpoint_eq_midpoint_iff_vsub_eq_vsub {x x' y y' : P} :
    midpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x x' y y' : P
⊢ midpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y

Tactic:
rw [← @vsub_eq_zero_iff_eq V, midpoint_vsub_midpoint, midpoint_eq_iff, pointReflection_apply,
  vsub_eq_sub, zero_sub, vadd_eq_add, add_zero, neg_eq_iff_eq_neg, neg_vsub_eq_vsub_rev]

Result:
no goals
-- Mathlib/GroupTheory/Torsion.lean
theorem IsTorsionFree.not_torsion [hN : Nontrivial G] : IsTorsionFree G → ¬IsTorsion G := fun tfG =>
  (not_isTorsion_iff _).mpr <| by
    obtain ⟨x, hx⟩ := (nontrivial_iff_exists_ne (1 : G)).mp hN
    exact ⟨x, (tfG x) hx⟩

Proof state:
G : Type u_1
inst✝ : Group G
hN : Nontrivial G
tfG : IsTorsionFree G
⊢ ∃ g, ¬IsOfFinOrder g

Tactic:
obtain ⟨x, hx⟩ := (nontrivial_iff_exists_ne (1 : G)).mp hN

Result:
case intro
G : Type u_1
inst✝ : Group G
hN : Nontrivial G
tfG : IsTorsionFree G
x : G
hx : x ≠ 1
⊢ ∃ g, ¬IsOfFinOrder g

Proof state:
case intro
G : Type u_1
inst✝ : Group G
hN : Nontrivial G
tfG : IsTorsionFree G
x : G
hx : x ≠ 1
⊢ ∃ g, ¬IsOfFinOrder g

Tactic:
exact ⟨x, (tfG x) hx⟩

Result:
no goals
-- Mathlib/RingTheory/PowerBasis.lean
theorem minpolyGen_map (pb : PowerBasis A S) (e : S ≃ₐ[A] S') :
    (pb.map e).minpolyGen = pb.minpolyGen

Proof state:
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
S' : Type u_7
inst✝² : CommRing S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
⊢ X ^ pb.dim - ∑ i : Fin pb.dim, C (((pb.map e).basis.repr ((pb.map e).gen ^ pb.dim)) i) * X ^ ↑i =
    X ^ pb.dim - ∑ i : Fin pb.dim, C ((pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i

Tactic:
simp only [LinearEquiv.trans_apply, map_basis, Basis.map_repr, map_gen,
  AlgEquiv.toLinearEquiv_apply, e.toLinearEquiv_symm, map_pow,
  AlgEquiv.symm_apply_apply, sub_right_inj]

Result:
no goals

Proof state:
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
S' : Type u_7
inst✝² : CommRing S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
⊢ (pb.map e).minpolyGen = pb.minpolyGen

Tactic:
dsimp only [minpolyGen, map_dim]

Result:
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
S' : Type u_7
inst✝² : CommRing S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
⊢ X ^ pb.dim - ∑ i : Fin pb.dim, C (((pb.map e).basis.repr ((pb.map e).gen ^ pb.dim)) i) * X ^ ↑i =
    X ^ pb.dim - ∑ i : Fin pb.dim, C ((pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i
-- Mathlib/Topology/AlexandrovDiscrete.lean
@[simp] lemma isOpen_exterior : IsOpen (exterior s)

Proof state:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s : Set α
⊢ IsOpen (exterior s)

Tactic:
rw [exterior_def]

Result:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s : Set α
⊢ IsOpen (⋂₀ {t | IsOpen t ∧ s ⊆ t})

Proof state:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s : Set α
⊢ IsOpen (⋂₀ {t | IsOpen t ∧ s ⊆ t})

Tactic:
exact isOpen_sInter fun _ ↦ And.left

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem norm_integral_le_of_norm_le {g : ℝ → ℝ} (h : ∀ᵐ t ∂μ.restrict <| Ι a b, ‖f t‖ ≤ g t)
    (hbound : IntervalIntegrable g μ a b) : ‖∫ t in a..b, f t ∂μ‖ ≤ |∫ t in a..b, g t ∂μ|

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
g : ℝ → ℝ
h : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖f t‖ ≤ g t
hbound : IntervalIntegrable g μ a b
⊢ ‖∫ (t : ℝ) in a..b, f t ∂μ‖ ≤ |∫ (t : ℝ) in a..b, g t ∂μ|

Tactic:
simp_rw [norm_intervalIntegral_eq, abs_intervalIntegral_eq,
  abs_eq_self.mpr (integral_nonneg_of_ae <| h.mono fun _t ht => (norm_nonneg _).trans ht),
  norm_integral_le_of_norm_le hbound.def' h]

Result:
no goals
-- Mathlib/FieldTheory/Laurent.lean
theorem laurent_C (x : R) : laurent r (C x) = C x

Proof state:
R : Type u
inst✝¹ : CommRing R
r : R
inst✝ : IsDomain R
x : R
⊢ (laurent r) (C x) = C x

Tactic:
rw [← algebraMap_C, laurent_algebraMap, taylor_C]

Result:
no goals
-- Mathlib/RingTheory/Kaehler/TensorProduct.lean
/--
If `B` is the tensor product of `S` and `A` over `R`,
then `Ω[B⁄S]` is the base change of `Ω[A⁄R]` along `R → S`.
-/
lemma isBaseChange [h : Algebra.IsPushout R S A B] :
    IsBaseChange S ((map R S A B).restrictScalars R)

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
⊢ IsBaseChange S (↑R (map R S A B))

Tactic:
convert (TensorProduct.isBaseChange R (Ω[A⁄R]) S).comp
  (IsBaseChange.ofEquiv (tensorKaehlerEquiv R S A B))

Result:
case h.e'_14
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
⊢ ↑R (map R S A B) = ↑R ↑(tensorKaehlerEquiv R S A B) ∘ₗ (mk R S (Ω[A⁄R])) 1

Proof state:
case h.e'_14
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
⊢ ↑R (map R S A B) = ↑R ↑(tensorKaehlerEquiv R S A B) ∘ₗ (mk R S (Ω[A⁄R])) 1

Tactic:
refine LinearMap.ext fun x ↦ ?_

Result:
case h.e'_14
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
x : Ω[A⁄R]
⊢ (↑R (map R S A B)) x = (↑R ↑(tensorKaehlerEquiv R S A B) ∘ₗ (mk R S (Ω[A⁄R])) 1) x

Proof state:
case h.e'_14
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
x : Ω[A⁄R]
⊢ (↑R (map R S A B)) x = (↑R ↑(tensorKaehlerEquiv R S A B) ∘ₗ (mk R S (Ω[A⁄R])) 1) x

Tactic:
simp only [LinearMap.coe_restrictScalars, LinearMap.coe_comp, LinearEquiv.coe_coe,
  Function.comp_apply, mk_apply, tensorKaehlerEquiv_tmul, one_smul]

Result:
no goals
-- Mathlib/Order/WithBot.lean
theorem coe_untopD_le (y : WithTop α) (a : α) : y.untopD a ≤ y :=  by cases y <;> simp

Proof state:
α : Type u_1
inst✝ : Preorder α
y : WithTop α
a : α
⊢ ↑(untopD a y) ≤ y

Tactic:
cases y <;> simp

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem expand (r : X) (s : S) (t : R) (hst : t * (s : R) ∈ S) :
    r /ₒ s = t • r /ₒ ⟨t * s, hst⟩

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s : ↥S
t : R
hst : t * ↑s ∈ S
⊢ r /ₒ s = t • r /ₒ ⟨t * ↑s, hst⟩

Tactic:
apply Quotient.sound

Result:
case a
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s : ↥S
t : R
hst : t * ↑s ∈ S
⊢ (r, s) ≈ (t • r, ⟨t * ↑s, hst⟩)

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s : ↥S
t : R
hst : t * ↑s ∈ S
⊢ ↑s * ↑(t • r, ⟨t * ↑s, hst⟩).2 = ↑s * t * ↑(r, s).2

Tactic:
rw [← mul_assoc]

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s : ↥S
t : R
hst : t * ↑s ∈ S
⊢ (r, s) ≈ (t • r, ⟨t * ↑s, hst⟩)

Tactic:
exact ⟨s, s * t, by rw [mul_smul, Submonoid.smul_def], by rw [← mul_assoc]⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s : ↥S
t : R
hst : t * ↑s ∈ S
⊢ s • (t • r, ⟨t * ↑s, hst⟩).1 = (↑s * t) • (r, s).1

Tactic:
rw [mul_smul, Submonoid.smul_def]

Result:
no goals
-- Mathlib/Analysis/Convex/EGauge.lean
@[simp] lemma egauge_empty (x : E) : egauge 𝕜 ∅ x = ∞

Proof state:
𝕜 : Type u_1
inst✝¹ : NNNorm 𝕜
E : Type u_2
inst✝ : SMul 𝕜 E
x : E
⊢ egauge 𝕜 ∅ x = ⊤

Tactic:
simp [egauge]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean
/-- Pull-out property of the conditional expectation. -/
lemma condExp_mul_of_stronglyMeasurable_right {f g : α → ℝ} (hg : StronglyMeasurable[m] g)
    (hfg : Integrable (f * g) μ) (hf : Integrable f μ) : μ[f * g | m] =ᵐ[μ] μ[f | m] * g

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hg : StronglyMeasurable g
hfg : Integrable (f * g) μ
hf : Integrable f μ
⊢ μ[f * g|m] =ᶠ[ae μ] μ[f|m] * g

Tactic:
simpa [mul_comm] using condExp_mul_of_stronglyMeasurable_left hg (mul_comm f g ▸ hfg) hf

Result:
no goals