harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem sub_neg_of_lt {a b : Int} (h : a < b) : a - b < 0

Proof state:
a b : Int
h : a < b
⊢ a - b < 0

Tactic:
have h := Int.add_lt_add_right h (-b)

Result:
a b : Int
h✝ : a < b
h : a + -b < b + -b
⊢ a - b < 0

Proof state:
a b : Int
h✝ : a < b
h : a + -b < b + -b
⊢ a - b < 0

Tactic:
rwa [Int.add_right_neg] at h

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem single_pow {b : ℕ} (_ : (a : R) ^ b = c) : (a + 0) ^ b = c + 0

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a c : R
b : ℕ
x✝ : a ^ b = c
⊢ (a + 0) ^ b = c + 0

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Data/Finsupp/SMul.lean
theorem comapSMul_apply (g : G) (f : α →₀ M) (a : α) : (g • f) a = f (g⁻¹ • a)

Proof state:
α : Type u_1
M : Type u_3
G : Type u_5
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g : G
f : α →₀ M
a : α
⊢ (g • f) a = f (g⁻¹ • a)

Tactic:
conv_lhs => rw [← smul_inv_smul g a]

Result:
α : Type u_1
M : Type u_3
G : Type u_5
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g : G
f : α →₀ M
a : α
⊢ (g • f) (g • g⁻¹ • a) = f (g⁻¹ • a)

Proof state:
α : Type u_1
M : Type u_3
G : Type u_5
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g : G
f : α →₀ M
a : α
⊢ (g • f) (g • g⁻¹ • a) = f (g⁻¹ • a)

Tactic:
exact mapDomain_apply (MulAction.injective g) _ (g⁻¹ • a)

Result:
no goals
-- Mathlib/Algebra/Homology/Single.lean
lemma isZero_single_obj_X (j : ι) (A : V) (i : ι) (hi : i ≠ j) :
    IsZero (((single V c j).obj A).X i)

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i : ι
hi : i ≠ j
⊢ IsZero (((single V c j).obj A).X i)

Tactic:
dsimp [single]

Result:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i : ι
hi : i ≠ j
⊢ IsZero (if i = j then A else 0)

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i : ι
hi : i ≠ j
⊢ IsZero (if i = j then A else 0)

Tactic:
rw [if_neg hi]

Result:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i : ι
hi : i ≠ j
⊢ IsZero 0

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i : ι
hi : i ≠ j
⊢ IsZero 0

Tactic:
exact Limits.isZero_zero V

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
@[simp]
lemma toQuotient_map : relations.toQuotient.comp relations.map = 0

Proof state:
A : Type u
inst✝ : Ring A
relations : Relations A
⊢ relations.toQuotient ∘ₗ relations.map = 0

Tactic:
aesop

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma P3.trans (h₁ : P3 x₁ x₂ y₁ y₂) (h₂ : P3 x₂ x₃ y₁ y₂) : P3 x₁ x₃ y₁ y₂

Proof state:
x₁ x₂ x₃ y₁ y₂ : PGame
h₁ : P3 x₁ x₂ y₁ y₂
h₂ : P3 x₂ x₃ y₁ y₂
⊢ P3 x₁ x₃ y₁ y₂

Tactic:
rw [P3] at h₁ h₂

Result:
x₁ x₂ x₃ y₁ y₂ : PGame
h₁ : ⟦x₁ * y₂⟧ + ⟦x₂ * y₁⟧ < ⟦x₁ * y₁⟧ + ⟦x₂ * y₂⟧
h₂ : ⟦x₂ * y₂⟧ + ⟦x₃ * y₁⟧ < ⟦x₂ * y₁⟧ + ⟦x₃ * y₂⟧
⊢ P3 x₁ x₃ y₁ y₂

Proof state:
x₁ x₂ x₃ y₁ y₂ : PGame
h₁ : ⟦x₁ * y₂⟧ + ⟦x₂ * y₁⟧ < ⟦x₁ * y₁⟧ + ⟦x₂ * y₂⟧
h₂ : ⟦x₂ * y₂⟧ + ⟦x₃ * y₁⟧ < ⟦x₂ * y₁⟧ + ⟦x₃ * y₂⟧
⊢ P3 x₁ x₃ y₁ y₂

Tactic:
rw [P3, ← add_lt_add_iff_left (⟦x₂ * y₁⟧ + ⟦x₂ * y₂⟧)]

Result:
x₁ x₂ x₃ y₁ y₂ : PGame
h₁ : ⟦x₁ * y₂⟧ + ⟦x₂ * y₁⟧ < ⟦x₁ * y₁⟧ + ⟦x₂ * y₂⟧
h₂ : ⟦x₂ * y₂⟧ + ⟦x₃ * y₁⟧ < ⟦x₂ * y₁⟧ + ⟦x₃ * y₂⟧
⊢ ⟦x₂ * y₁⟧ + ⟦x₂ * y₂⟧ + (⟦x₁ * y₂⟧ + ⟦x₃ * y₁⟧) < ⟦x₂ * y₁⟧ + ⟦x₂ * y₂⟧ + (⟦x₁ * y₁⟧ + ⟦x₃ * y₂⟧)

Proof state:
x₁ x₂ x₃ y₁ y₂ : PGame
h₁ : ⟦x₁ * y₂⟧ + ⟦x₂ * y₁⟧ < ⟦x₁ * y₁⟧ + ⟦x₂ * y₂⟧
h₂ : ⟦x₂ * y₂⟧ + ⟦x₃ * y₁⟧ < ⟦x₂ * y₁⟧ + ⟦x₃ * y₂⟧
⊢ ⟦x₂ * y₁⟧ + ⟦x₂ * y₂⟧ + (⟦x₁ * y₂⟧ + ⟦x₃ * y₁⟧) < ⟦x₂ * y₁⟧ + ⟦x₂ * y₂⟧ + (⟦x₁ * y₁⟧ + ⟦x₃ * y₂⟧)

Tactic:
convert add_lt_add h₁ h₂ using 1 <;> abel

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_fiberwise' [DecidableEq κ] (g : ι → κ) (f : κ → α) :
    ∏ j, ∏ _i : {i // g i = j}, f j = ∏ i, f (g i)

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid α
inst✝ : DecidableEq κ
g : ι → κ
f : κ → α
⊢ ∏ j : κ, ∏ _i : { i // g i = j }, f j = ∏ i : ι, f (g i)

Tactic:
rw [← Finset.prod_fiberwise' _ g f]

Result:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid α
inst✝ : DecidableEq κ
g : ι → κ
f : κ → α
⊢ ∏ j : κ, ∏ _i : { i // g i = j }, f j = ∏ j : κ, ∏ i ∈ filter (fun i => g i = j) univ, f j

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid α
inst✝ : DecidableEq κ
g : ι → κ
f : κ → α
⊢ ∏ j : κ, ∏ _i : { i // g i = j }, f j = ∏ j : κ, ∏ i ∈ filter (fun i => g i = j) univ, f j

Tactic:
congr with j

Result:
case e_f.h
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid α
inst✝ : DecidableEq κ
g : ι → κ
f : κ → α
j : κ
⊢ ∏ _i : { i // g i = j }, f j = ∏ i ∈ filter (fun i => g i = j) univ, f j

Proof state:
case e_f.h
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid α
inst✝ : DecidableEq κ
g : ι → κ
f : κ → α
j : κ
⊢ ∏ _i : { i // g i = j }, f j = ∏ i ∈ filter (fun i => g i = j) univ, f j

Tactic:
exact (prod_subtype _ (by simp) fun _ ↦ _).symm

Result:
no goals

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid α
inst✝ : DecidableEq κ
g : ι → κ
f : κ → α
j : κ
⊢ ∀ (x : ι), x ∈ filter (fun i => g i = j) univ ↔ g x = j

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Equiv.lean
theorem inverse_equiv (e : M ≃L[R] M₂) : inverse (e : M →L[R] M₂) = e.symm

Proof state:
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
⊢ (↑e).inverse = ↑e.symm

Tactic:
simp [inverse]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem iso_symm_apply' (m : M') (a : M) (b : S) (eq1 : b • m = f a) :
    (iso S f).symm m = LocalizedModule.mk a b :=
  (iso_symm_apply_aux S f m).trans <|
    LocalizedModule.mk_eq.mpr <| by
      rw [← IsLocalizedModule.eq_iff_exists S f, Submonoid.smul_def, Submonoid.smul_def, f.map_smul,
        f.map_smul, ← (surj' _).choose_spec, ← Submonoid.smul_def, ← Submonoid.smul_def, ← mul_smul,
        mul_comm, mul_smul, eq1]

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M'
a : M
b : ↥S
eq1 : b • m = f a
⊢ ∃ u, u • b • ⋯.choose.1 = u • ⋯.choose.2 • a

Tactic:
rw [← IsLocalizedModule.eq_iff_exists S f, Submonoid.smul_def, Submonoid.smul_def, f.map_smul,
  f.map_smul, ← (surj' _).choose_spec, ← Submonoid.smul_def, ← Submonoid.smul_def, ← mul_smul,
  mul_comm, mul_smul, eq1]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Basic.lean
theorem mk_apply_of_not_mem {s : Finset ι} {f : ∀ i : (↑s : Set ι), β i.val} {n : ι} (hn : n ∉ s) :
    mk β s f n = 0

Proof state:
ι : Type v
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : DecidableEq ι
s : Finset ι
f : (i : ↑↑s) → β ↑i
n : ι
hn : n ∉ s
⊢ (if H : n ∈ s then f ⟨n, H⟩ else 0) = 0

Tactic:
rw [dif_neg hn]

Result:
no goals

Proof state:
ι : Type v
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : DecidableEq ι
s : Finset ι
f : (i : ↑↑s) → β ↑i
n : ι
hn : n ∉ s
⊢ ((mk β s) f) n = 0

Tactic:
dsimp only [Finset.coe_sort_coe, mk, AddMonoidHom.coe_mk, ZeroHom.coe_mk, DFinsupp.mk_apply]

Result:
ι : Type v
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : DecidableEq ι
s : Finset ι
f : (i : ↑↑s) → β ↑i
n : ι
hn : n ∉ s
⊢ (if H : n ∈ s then f ⟨n, H⟩ else 0) = 0
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem mem_support_not_mem_vars_zero {f : MvPolynomial σ R} {x : σ →₀ ℕ} (H : x ∈ f.support)
    {v : σ} (h : v ∉ vars f) : x v = 0

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ f.support
v : σ
h : v ∉ f.vars
⊢ x v = 0

Tactic:
contrapose! h

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ f.support
v : σ
h : x v ≠ 0
⊢ v ∈ f.vars

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ f.support
v : σ
h : x v ≠ 0
⊢ v ∈ f.vars

Tactic:
exact (mem_vars v).mpr ⟨x, H, Finsupp.mem_support_iff.mpr h⟩

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem norm_div_sin_oangle_add_right_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : ‖y‖ / Real.Angle.sin (o.oangle x (x + y)) = ‖x + y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ ‖y‖ / (o.oangle x (x + y)).sin = ‖x + y‖

Tactic:
have hs : (o.oangle x (x + y)).sign = 1 := by
  rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ ‖y‖ / (o.oangle x (x + y)).sin = ‖x + y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ ‖y‖ / (o.oangle x (x + y)).sin = ‖x + y‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
  InnerProductGeometry.norm_div_sin_angle_add_of_inner_eq_zero
    (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inr (o.right_ne_zero_of_oangle_eq_pi_div_two h))]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle x (x + y)).sign = 1

Tactic:
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem sin_oangle_sub_left_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    Real.Angle.sin (o.oangle (x - y) x) = ‖y‖ / ‖x - y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle (x - y) x).sin = ‖y‖ / ‖x - y‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle x (x - y)).sin = ‖y‖ / ‖x - y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle x (x - y)).sin = ‖y‖ / ‖x - y‖

Tactic:
exact (-o).sin_oangle_sub_right_of_oangle_eq_pi_div_two h

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem lift_eq (x : M) : f.lift hg (f.toMap x) = g x

Proof state:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
⊢ (f.lift hg) (f.toMap x) = g x

Tactic:
rw [lift_spec, ← g.map_mul]

Result:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
⊢ g (f.sec (f.toMap x)).1 = g (↑(f.sec (f.toMap x)).2 * x)

Proof state:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
⊢ g (f.sec (f.toMap x)).1 = g (↑(f.sec (f.toMap x)).2 * x)

Tactic:
exact f.eq_of_eq hg (by rw [sec_spec', f.toMap.map_mul])

Result:
no goals

Proof state:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
⊢ f.toMap (f.sec (f.toMap x)).1 = f.toMap (↑(f.sec (f.toMap x)).2 * x)

Tactic:
rw [sec_spec', f.toMap.map_mul]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addXYZ_self {P : Fin 3 → R} (hP : W'.Equation P) : W'.addXYZ P P = ![0, 0, 0]

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.addXYZ P P = ![0, 0, 0]

Tactic:
rw [addXYZ, addX_self hP, addY_self hP, addZ_self]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem wbtw_self_iff {x y : P} : Wbtw R x y x ↔ y = x

Proof state:
case refine_2
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : y = x
⊢ Wbtw R x y x

Tactic:
rw [h]

Result:
case refine_2
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : y = x
⊢ Wbtw R x x x

Proof state:
case refine_1
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : Wbtw R x y x
⊢ y = x

Tactic:
have ⟨_, _, h₂⟩ := h

Result:
case refine_1
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : Wbtw R x y x
w✝ : R
left✝ : w✝ ∈ Set.Icc 0 1
h₂ : (lineMap x x) w✝ = y
⊢ y = x

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ Wbtw R x y x ↔ y = x

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

Result:
case refine_1
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : Wbtw R x y x
⊢ y = x

case refine_2
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : y = x
⊢ Wbtw R x y x

Proof state:
case refine_1
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : Wbtw R x y x
w✝ : R
left✝ : w✝ ∈ Set.Icc 0 1
h₂ : (lineMap x x) w✝ = y
⊢ y = x

Tactic:
rw [h₂.symm, lineMap_same_apply]

Result:
no goals

Proof state:
case refine_2
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : y = x
⊢ Wbtw R x x x

Tactic:
exact wbtw_self_left R x x

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma indep_iff_forall_not_mem_closure_diff (hI : I ⊆ M.E

Proof state:
case mpr
α : Type u_2
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
⊢ (∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})) → M.Indep I

Tactic:
intro h

Result:
case mpr
α : Type u_2
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
⊢ M.Indep I

Proof state:
α : Type u_2
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
⊢ M.Indep I ↔ ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})

Tactic:
use fun h e heI he ↦ ((h.closure_inter_eq_self_of_subset diff_subset).subset ⟨he, heI⟩).2 rfl

Result:
case mpr
α : Type u_2
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
⊢ (∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})) → M.Indep I

Proof state:
case h.e'_3
α : Type u_2
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
J : Set α
hJ : M.IsBasis J I
⊢ I = J

Tactic:
refine hJ.subset.antisymm' (fun e he ↦ by_contra fun heJ ↦ h he ?_)

Result:
case h.e'_3
α : Type u_2
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
J : Set α
hJ : M.IsBasis J I
e : α
he : e ∈ I
heJ : e ∉ J
⊢ e ∈ M.closure (I \ {e})

Proof state:
case h.e'_3
α : Type u_2
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
J : Set α
hJ : M.IsBasis J I
e : α
he : e ∈ I
heJ : e ∉ J
⊢ e ∈ M.closure (I \ {e})

Tactic:
exact mem_of_mem_of_subset
  (hJ.subset_closure he) (M.closure_subset_closure (subset_diff_singleton hJ.subset heJ))

Result:
no goals

Proof state:
case mpr
α : Type u_2
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
⊢ M.Indep I

Tactic:
obtain ⟨J, hJ⟩ := M.exists_isBasis I

Result:
case mpr.intro
α : Type u_2
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
J : Set α
hJ : M.IsBasis J I
⊢ M.Indep I

Proof state:
case mpr.intro
α : Type u_2
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
J : Set α
hJ : M.IsBasis J I
⊢ M.Indep I

Tactic:
convert hJ.indep

Result:
case h.e'_3
α : Type u_2
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
J : Set α
hJ : M.IsBasis J I
⊢ I = J
-- Mathlib/Algebra/Group/Submonoid/MulOpposite.lean
theorem unop_closure (s : Set Mᵐᵒᵖ) : (closure s).unop = closure (MulOpposite.op ⁻¹' s)

Proof state:
M : Type u_2
inst✝ : MulOneClass M
s : Set Mᵐᵒᵖ
⊢ (closure s).unop = closure (MulOpposite.op ⁻¹' s)

Tactic:
rw [← op_inj, op_unop, op_closure]

Result:
M : Type u_2
inst✝ : MulOneClass M
s : Set Mᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' (MulOpposite.op ⁻¹' s))

Proof state:
M : Type u_2
inst✝ : MulOneClass M
s : Set Mᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' (MulOpposite.op ⁻¹' s))

Tactic:
simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isEmpty_modifyKey [BEq α] [LawfulBEq α] (k : α) (f : β k → β k) (l : List ((a : α) × β a)) :
    (modifyKey k f l).isEmpty = l.isEmpty

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
l : List ((a : α) × β a)
a : (a : α) × β a
as : List ((a : α) × β a)
⊢ (modifyKey k f (a :: as)).isEmpty = (a :: as).isEmpty

Tactic:
simp only [modifyKey, replaceEntry, cond_eq_if]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
l : List ((a : α) × β a)
a : (a : α) × β a
as : List ((a : α) × β a)
⊢ (match getValueCast? k (a :: as) with
      | none => a :: as
      | some v => if (a.fst == k) = true then ⟨k, f v⟩ :: as else ⟨a.fst, a.snd⟩ :: replaceEntry k (f v) as).isEmpty =
    (a :: as).isEmpty

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
l : List ((a : α) × β a)
a : (a : α) × β a
as : List ((a : α) × β a)
⊢ (match getValueCast? k (a :: as) with
      | none => a :: as
      | some v => if (a.fst == k) = true then ⟨k, f v⟩ :: as else ⟨a.fst, a.snd⟩ :: replaceEntry k (f v) as).isEmpty =
    (a :: as).isEmpty

Tactic:
repeat' split <;> simp

Result:
no goals

Proof state:
case h_2
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
l : List ((a : α) × β a)
a : (a : α) × β a
as : List ((a : α) × β a)
x✝ : Option (β k)
v✝ : β k
heq✝ : getValueCast? k (a :: as) = some v✝
⊢ (if (a.fst == k) = true then ⟨k, f v✝⟩ :: as else ⟨a.fst, a.snd⟩ :: replaceEntry k (f v✝) as).isEmpty = false

Tactic:
split <;> simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
l : List ((a : α) × β a)
⊢ (modifyKey k f l).isEmpty = l.isEmpty

Tactic:
match l with
| [] => simp [modifyKey]
| a :: as =>
  simp only [modifyKey, replaceEntry, cond_eq_if]
  repeat' split <;> simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
l : List ((a : α) × β a)
⊢ (modifyKey k f []).isEmpty = [].isEmpty

Tactic:
simp [modifyKey]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
lemma measure_support_lt_top_of_lintegral_ne_top {f : α →ₛ ℝ≥0∞} (hf : f.lintegral μ ≠ ∞) :
    μ (support f) < ∞

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hf : f.lintegral μ ≠ ⊤
⊢ f.FinMeasSupp μ

Tactic:
exact FinMeasSupp.of_lintegral_ne_top hf

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hf : f.lintegral μ ≠ ⊤
⊢ μ (support ⇑f) < ⊤

Tactic:
refine measure_support_lt_top f ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hf : f.lintegral μ ≠ ⊤
⊢ ∀ (y : ℝ≥0∞), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hf : f.lintegral μ ≠ ⊤
⊢ ∀ (y : ℝ≥0∞), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
rw [← finMeasSupp_iff]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hf : f.lintegral μ ≠ ⊤
⊢ f.FinMeasSupp μ
-- Mathlib/Algebra/Lie/Submodule.lean
theorem Submodule.exists_lieSubmodule_coe_eq_iff (p : Submodule R M) :
    (∃ N : LieSubmodule R L M, ↑N = p) ↔ ∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p

Proof state:
case mp
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
⊢ (∃ N, ↑N = p) → ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p

Tactic:
rintro ⟨N, rfl⟩ _ _

Result:
case mp.intro
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
x✝ : L
m✝ : M
⊢ m✝ ∈ ↑N → ⁅x✝, m✝⁆ ∈ ↑N

Proof state:
case mp.intro
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
x✝ : L
m✝ : M
⊢ m✝ ∈ ↑N → ⁅x✝, m✝⁆ ∈ ↑N

Tactic:
exact N.lie_mem

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
⊢ (∃ N, ↑N = p) ↔ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p

Tactic:
constructor

Result:
case mp
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
⊢ (∃ N, ↑N = p) → ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p

case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
⊢ (∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p) → ∃ N, ↑N = p

Proof state:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
h : ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
⊢ ∃ N, ↑N = p

Tactic:
use { p with lie_mem := @h }

Result:
no goals

Proof state:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
⊢ (∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p) → ∃ N, ↑N = p

Tactic:
intro h

Result:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
p : Submodule R M
h : ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
⊢ ∃ N, ↑N = p