harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma rnDeriv_mul_rnDeriv {κ : Measure α} [SigmaFinite μ] [SigmaFinite ν] [SigmaFinite κ]
    (hμν : μ ≪ ν) :
    μ.rnDeriv ν * ν.rnDeriv κ =ᵐ[κ] μ.rnDeriv κ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hμν : μ ≪ ν
⊢ μ.rnDeriv ν * ν.rnDeriv κ =ᶠ[ae κ] μ.rnDeriv κ

Tactic:
refine (rnDeriv_withDensity_left ?_ ?_).symm.trans ?_

Result:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hμν : μ ≪ ν
⊢ AEMeasurable (μ.rnDeriv ν) κ

case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hμν : μ ≪ ν
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ ⊤

case refine_3
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hμν : μ ≪ ν
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ =ᶠ[ae κ] μ.rnDeriv κ

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hμν : μ ≪ ν
⊢ AEMeasurable (μ.rnDeriv ν) κ

Tactic:
exact (Measure.measurable_rnDeriv _ _).aemeasurable

Result:
no goals

Proof state:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hμν : μ ≪ ν
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ ⊤

Tactic:
exact rnDeriv_ne_top _ _

Result:
no goals

Proof state:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hμν : μ ≪ ν
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ =ᶠ[ae κ] μ.rnDeriv κ

Tactic:
rw [Measure.withDensity_rnDeriv_eq _ _ hμν]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/FractionalIdeal.lean
theorem mem_span_basisOfFractionalIdeal {I : (FractionalIdeal (𝓞 K)⁰ K)ˣ} {x : K} :
    x ∈ Submodule.span ℤ (Set.range (basisOfFractionalIdeal K I)) ↔ x ∈ (I : Set K)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : K
⊢ x ∈ LinearMap.range (↑ℤ (↑↑I).subtype) ↔ x ∈ ↑↑I

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : K
⊢ x ∈ Submodule.span ℤ (Set.range ⇑(basisOfFractionalIdeal K I)) ↔ x ∈ ↑↑I

Tactic:
rw [basisOfFractionalIdeal, (fractionalIdealBasis K I.1).ofIsLocalizedModule_span ℚ ℤ⁰ _]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : K
⊢ x ∈ LinearMap.range (↑ℤ (↑↑I).subtype) ↔ x ∈ ↑↑I
-- Mathlib/Data/List/Scan.lean
theorem getElem?_scanl_zero : (scanl f b l)[0]? = some b

Proof state:
case cons
α : Type u_1
β : Type u_2
f : β → α → β
b : β
head✝ : α
tail✝ : List α
⊢ (scanl f b (head✝ :: tail✝))[0]? = some b

Tactic:
simp [scanl_cons, singleton_append]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
f : β → α → β
b : β
⊢ (scanl f b [])[0]? = some b

Tactic:
simp [scanl_nil]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : β → α → β
b : β
l : List α
⊢ (scanl f b l)[0]? = some b

Tactic:
cases l

Result:
case nil
α : Type u_1
β : Type u_2
f : β → α → β
b : β
⊢ (scanl f b [])[0]? = some b

case cons
α : Type u_1
β : Type u_2
f : β → α → β
b : β
head✝ : α
tail✝ : List α
⊢ (scanl f b (head✝ :: tail✝))[0]? = some b
-- Mathlib/GroupTheory/DoubleCoset.lean
theorem doset_union_leftCoset (H K : Subgroup G) (a : G) :
    ⋃ h : H, (h * a : G) • ↑K = doset a H K

Proof state:
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑K
hxy : x✝ = x * a * y
⊢ ∃ i, a⁻¹ * (↑i)⁻¹ * x✝ ∈ ↑K

Tactic:
refine ⟨⟨x, hx⟩, ?_⟩

Result:
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑K
hxy : x✝ = x * a * y
⊢ a⁻¹ * (↑⟨x, hx⟩)⁻¹ * x✝ ∈ ↑K

Proof state:
case h.mpr
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ (∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * a * y) → ∃ i, a⁻¹ * (↑i)⁻¹ * x ∈ ↑K

Tactic:
rintro ⟨x, hx, y, hy, hxy⟩

Result:
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑K
hxy : x✝ = x * a * y
⊢ ∃ i, a⁻¹ * (↑i)⁻¹ * x✝ ∈ ↑K

Proof state:
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑K
hxy : x✝ = x * a * y
⊢ a⁻¹ * (↑⟨x, hx⟩)⁻¹ * x✝ ∈ ↑K

Tactic:
simp only [hxy, ← mul_assoc, hy, one_mul, inv_mul_cancel, Subgroup.coe_mk, inv_mul_cancel_right]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a : G
⊢ ⋃ h, (↑h * a) • ↑K = doset a ↑H ↑K

Tactic:
ext x

Result:
case h
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ x ∈ ⋃ h, (↑h * a) • ↑K ↔ x ∈ doset a ↑H ↑K

Proof state:
case h.mp
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ (∃ i, a⁻¹ * (↑i)⁻¹ * x ∈ ↑K) → ∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * a * y

Tactic:
rintro ⟨y, h_h⟩

Result:
case h.mp.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
y : ↥H
h_h : a⁻¹ * (↑y)⁻¹ * x ∈ ↑K
⊢ ∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * a * y

Proof state:
case h.mp.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
y : ↥H
h_h : a⁻¹ * (↑y)⁻¹ * x ∈ ↑K
⊢ x = ↑y * a * (a⁻¹ * ↑y⁻¹ * x)

Tactic:
simp only [← mul_assoc, one_mul, mul_inv_cancel, mul_inv_cancel_right, InvMemClass.coe_inv]

Result:
no goals

Proof state:
case h
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ (∃ i, a⁻¹ * (↑i)⁻¹ * x ∈ ↑K) ↔ ∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * a * y

Tactic:
constructor

Result:
case h.mp
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ (∃ i, a⁻¹ * (↑i)⁻¹ * x ∈ ↑K) → ∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * a * y

case h.mpr
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ (∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * a * y) → ∃ i, a⁻¹ * (↑i)⁻¹ * x ∈ ↑K

Proof state:
case h
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ x ∈ ⋃ h, (↑h * a) • ↑K ↔ x ∈ doset a ↑H ↑K

Tactic:
simp only [mem_leftCoset_iff, mul_inv_rev, Set.mem_iUnion, mem_doset]

Result:
case h
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ (∃ i, a⁻¹ * (↑i)⁻¹ * x ∈ ↑K) ↔ ∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * a * y

Proof state:
case h.mp.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
y : ↥H
h_h : a⁻¹ * (↑y)⁻¹ * x ∈ ↑K
⊢ ∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * a * y

Tactic:
refine ⟨y, y.2, a⁻¹ * y⁻¹ * x, h_h, ?_⟩

Result:
case h.mp.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
y : ↥H
h_h : a⁻¹ * (↑y)⁻¹ * x ∈ ↑K
⊢ x = ↑y * a * (a⁻¹ * ↑y⁻¹ * x)
-- Mathlib/.lake/packages/batteries/Batteries/Classes/Order.lean
theorem cmp_eq_eq_symm [OrientedCmp cmp] : cmp x y = .eq ↔ cmp y x = .eq

Proof state:
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
x y : α✝
inst✝ : OrientedCmp cmp
⊢ cmp y x = Ordering.eq.swap ↔ cmp y x = Ordering.eq

Tactic:
exact .rfl

Result:
no goals

Proof state:
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
x y : α✝
inst✝ : OrientedCmp cmp
⊢ cmp x y = Ordering.eq ↔ cmp y x = Ordering.eq

Tactic:
rw [← Ordering.swap_inj, symm]

Result:
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
x y : α✝
inst✝ : OrientedCmp cmp
⊢ cmp y x = Ordering.eq.swap ↔ cmp y x = Ordering.eq
-- Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
/-- Extensionality theorem for `FixedDetMatrix` with respect to the underlying matrix, not
entriwise. -/
lemma ext' {m : R} {A B : FixedDetMatrix n R m} (h : A.1 = B.1) : A = B

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
A B : FixedDetMatrix n R m
h : ↑A = ↑B
⊢ A = B

Tactic:
cases A

Result:
case mk
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
B : FixedDetMatrix n R m
val✝ : Matrix n n R
property✝ : val✝.det = m
h : ↑⟨val✝, property✝⟩ = ↑B
⊢ ⟨val✝, property✝⟩ = B

Proof state:
case mk
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
B : FixedDetMatrix n R m
val✝ : Matrix n n R
property✝ : val✝.det = m
h : ↑⟨val✝, property✝⟩ = ↑B
⊢ ⟨val✝, property✝⟩ = B

Tactic:
cases B

Result:
case mk.mk
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
val✝¹ : Matrix n n R
property✝¹ : val✝¹.det = m
val✝ : Matrix n n R
property✝ : val✝.det = m
h : ↑⟨val✝¹, property✝¹⟩ = ↑⟨val✝, property✝⟩
⊢ ⟨val✝¹, property✝¹⟩ = ⟨val✝, property✝⟩

Proof state:
case mk.mk
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
val✝¹ : Matrix n n R
property✝¹ : val✝¹.det = m
val✝ : Matrix n n R
property✝ : val✝.det = m
h : ↑⟨val✝¹, property✝¹⟩ = ↑⟨val✝, property✝⟩
⊢ ⟨val✝¹, property✝¹⟩ = ⟨val✝, property✝⟩

Tactic:
congr

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem cos_neg (θ : Angle) : cos (-θ) = cos θ

Proof state:
θ : Angle
⊢ (-θ).cos = θ.cos

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
x✝ : ℝ
⊢ (-↑x✝).cos = (↑x✝).cos

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

Tactic:
exact Real.cos_neg _

Result:
no goals
-- Mathlib/GroupTheory/Coprod/Basic.lean
theorem fst_prod_snd : (fst : M ∗ N →* M).prod snd = toProd

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ fst.prod snd = toProd

Tactic:
ext1 <;> rfl

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem Tendsto.isCompact_insert_range_of_cofinite {f : ι → X} {x} (hf : Tendsto f cofinite (𝓝 x)) :
    IsCompact (insert x (range f))

Proof state:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
f : ι → X
x : X
this : TopologicalSpace ι := ⊥
hf : Tendsto f (cocompact ι) (𝓝 x)
h : DiscreteTopology ι
⊢ IsCompact (insert x (range f))

Tactic:
exact hf.isCompact_insert_range_of_cocompact continuous_of_discreteTopology

Result:
no goals

Proof state:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
f : ι → X
x : X
hf : Tendsto f cofinite (𝓝 x)
⊢ IsCompact (insert x (range f))

Tactic:
letI : TopologicalSpace ι := ⊥

Result:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
f : ι → X
x : X
hf : Tendsto f cofinite (𝓝 x)
this : TopologicalSpace ι := ⊥
⊢ IsCompact (insert x (range f))

Proof state:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
f : ι → X
x : X
hf : Tendsto f cofinite (𝓝 x)
this : TopologicalSpace ι := ⊥
⊢ IsCompact (insert x (range f))

Tactic:
haveI h : DiscreteTopology ι := ⟨rfl⟩

Result:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
f : ι → X
x : X
hf : Tendsto f cofinite (𝓝 x)
this : TopologicalSpace ι := ⊥
h : DiscreteTopology ι
⊢ IsCompact (insert x (range f))

Proof state:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
f : ι → X
x : X
hf : Tendsto f cofinite (𝓝 x)
this : TopologicalSpace ι := ⊥
h : DiscreteTopology ι
⊢ IsCompact (insert x (range f))

Tactic:
rw [← cocompact_eq_cofinite ι] at hf

Result:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
f : ι → X
x : X
this : TopologicalSpace ι := ⊥
hf : Tendsto f (cocompact ι) (𝓝 x)
h : DiscreteTopology ι
⊢ IsCompact (insert x (range f))
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem norm_div_cos_oangle_add_left_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : ‖y‖ / Real.Angle.cos (o.oangle (x + y) 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 + y) y).cos = ‖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)
⊢ ‖y‖ / ((-o).oangle y (x + y)).cos = ‖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)
⊢ ‖y‖ / ((-o).oangle y (y + x)).cos = ‖y + x‖

Tactic:
exact (-o).norm_div_cos_oangle_add_right_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 y x = ↑(π / 2)
⊢ ‖y‖ / ((-o).oangle y (x + y)).cos = ‖x + y‖

Tactic:
rw [add_comm]

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)
⊢ ‖y‖ / ((-o).oangle y (y + x)).cos = ‖y + x‖
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem affineIndependent_set_iff_linearIndependent_vsub {s : Set P} {p₁ : P} (hp₁ : p₁ ∈ s) :
    AffineIndependent k (fun p => p : s → P) ↔
      LinearIndependent k (fun v => v : (fun p => (p -ᵥ p₁ : V)) '' (s \ {p₁}) → V)

Proof state:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (LinearIndependent k fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩) →
    LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v

Tactic:
intro h

Result:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩
⊢ LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v

Proof state:
case h.e'_4.h.h.e
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩
hv : ∀ (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))), ↑v +ᵥ p₁ ∈ s \ {p₁}
f : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁})) → { x // x ≠ ⟨p₁, hp₁⟩ } := fun x => ⟨⟨↑x +ᵥ p₁, ⋯⟩, ⋯⟩
x✝ : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))
⊢ Subtype.val = (fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩) ∘ f

Tactic:
ext v

Result:
case h.e'_4.h.h.e.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩
hv : ∀ (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))), ↑v +ᵥ p₁ ∈ s \ {p₁}
f : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁})) → { x // x ≠ ⟨p₁, hp₁⟩ } := fun x => ⟨⟨↑x +ᵥ p₁, ⋯⟩, ⋯⟩
x✝ : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))
v : { x // x ∈ (fun p => p -ᵥ p₁) '' (s \ {p₁}) }
⊢ ↑v = ((fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩) ∘ f) v
-- Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean
theorem exists_finset (x : M ⊗[R] N) :
    ∃ S : Finset (M × N), x = S.sum fun i ↦ i.1 ⊗ₜ[R] i.2

Proof state:
case intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n => m ⊗ₜ[R] n
⊢ ∃ S, x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2

Tactic:
use S.graph

Result:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n => m ⊗ₜ[R] n
⊢ x = ∑ i ∈ S.graph, i.1 ⊗ₜ[R] i.2

Proof state:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n => m ⊗ₜ[R] n
⊢ ∑ a ∈ S.support, a ⊗ₜ[R] S a = ∑ i ∈ S.graph, i.1 ⊗ₜ[R] i.2

Tactic:
apply Finset.sum_nbij' (fun m ↦ ⟨m, S m⟩) Prod.fst <;> simp

Result:
no goals

Proof state:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n => m ⊗ₜ[R] n
⊢ x = ∑ i ∈ S.graph, i.1 ⊗ₜ[R] i.2

Tactic:
rw [h, Finsupp.sum]

Result:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n => m ⊗ₜ[R] n
⊢ ∑ a ∈ S.support, a ⊗ₜ[R] S a = ∑ i ∈ S.graph, i.1 ⊗ₜ[R] i.2

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
⊢ ∃ S, x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2

Tactic:
obtain ⟨S, h⟩ := exists_finsupp_left x

Result:
case intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n => m ⊗ₜ[R] n
⊢ ∃ S, x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
-- Mathlib/RingTheory/NonUnitalSubring/Basic.lean
theorem map_iInf {ι : Sort*} [Nonempty ι] (f : F) (hf : Function.Injective f)
    (s : ι → NonUnitalSubring R) : (iInf s).map f = ⨅ i, (s i).map f

Proof state:
F : Type w
R : Type u
S : Type v
inst✝⁴ : NonUnitalNonAssocRing R
inst✝³ : NonUnitalNonAssocRing S
inst✝² : FunLike F R S
inst✝¹ : NonUnitalRingHomClass F R S
ι : Sort u_1
inst✝ : Nonempty ι
f : F
hf : Function.Injective ⇑f
s : ι → NonUnitalSubring R
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective

Result:
case a
F : Type w
R : Type u
S : Type v
inst✝⁴ : NonUnitalNonAssocRing R
inst✝³ : NonUnitalNonAssocRing S
inst✝² : FunLike F R S
inst✝¹ : NonUnitalRingHomClass F R S
ι : Sort u_1
inst✝ : Nonempty ι
f : F
hf : Function.Injective ⇑f
s : ι → NonUnitalSubring R
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Proof state:
case a
F : Type w
R : Type u
S : Type v
inst✝⁴ : NonUnitalNonAssocRing R
inst✝³ : NonUnitalNonAssocRing S
inst✝² : FunLike F R S
inst✝¹ : NonUnitalRingHomClass F R S
ι : Sort u_1
inst✝ : Nonempty ι
f : F
hf : Function.Injective ⇑f
s : ι → NonUnitalSubring R
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem singleton_one [h : IsCyclotomicExtension {1} A B] : (⊥ : Subalgebra A B) = ⊤ :=
  Algebra.eq_top_iff.2 fun x => by
    simpa [adjoin_singleton_one] using ((isCyclotomicExtension_iff _ _ _).1 h).2 x

Proof state:
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension {1} A B
x : B
⊢ x ∈ ⊥

Tactic:
simpa [adjoin_singleton_one] using ((isCyclotomicExtension_iff _ _ _).1 h).2 x

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Nilpotent.lean
theorem Ideal.isRadical_iff_quotient_reduced {R : Type*} [CommRing R] (I : Ideal R) :
    I.IsRadical ↔ IsReduced (R ⧸ I)

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ I.IsRadical ↔ IsReduced (R ⧸ I)

Tactic:
conv_lhs => rw [← @Ideal.mk_ker R _ I]

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ (RingHom.ker (Quotient.mk I)).IsRadical ↔ IsReduced (R ⧸ I)

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ (RingHom.ker (Quotient.mk I)).IsRadical ↔ IsReduced (R ⧸ I)

Tactic:
exact RingHom.ker_isRadical_iff_reduced_of_surjective Quotient.mk_surjective

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem _root_.Matrix.separatingLeft_toLinearMap₂_iff {M : Matrix ι ι R₁} (b : Basis ι R₁ M₁) :
    (toLinearMap₂ b b M).SeparatingLeft ↔ M.Nondegenerate

Proof state:
R₁ : Type u_2
M₁ : Type u_6
ι : Type u_15
inst✝⁴ : CommRing R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
M : Matrix ι ι R₁
b : Basis ι R₁ M₁
⊢ ((toLinearMap₂ b b) M).SeparatingLeft ↔ M.Nondegenerate

Tactic:
rw [← Matrix.separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂,
  Matrix.separatingLeft_toLinearMap₂'_iff]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem add_mul_left_left (h : IsRelPrime x y) (z : R) : IsRelPrime (x + y * z) y :=
  @of_add_mul_left_left R _ _ _ (-z) <| by simpa only [mul_neg, add_neg_cancel_right] using h

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : R
h : IsRelPrime x y
z : R
⊢ IsRelPrime (x + y * z + y * -z) y

Tactic:
simpa only [mul_neg, add_neg_cancel_right] using h

Result:
no goals
-- Mathlib/Order/Filter/FilterProduct.lean
theorem min_def [K : LinearOrder β] (x y : β*) : min x y = map₂ min x y :=
  inductionOn₂ x y fun a b => by
    rcases le_total (a : β*) b with h | h
    · rw [min_eq_left h, map₂_coe, coe_eq]
      exact h.mono fun i hi => (min_eq_left hi).symm
    · rw [min_eq_right h, map₂_coe, coe_eq]
      exact h.mono fun i hi => (min_eq_right hi).symm

Proof state:
case inr
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑b ≤ ↑a
⊢ b =ᶠ[↑φ] fun x => a x ⊓ b x

Tactic:
exact h.mono fun i hi => (min_eq_right hi).symm

Result:
no goals

Proof state:
case inr
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑b ≤ ↑a
⊢ ↑a ⊓ ↑b = map₂ min ↑a ↑b

Tactic:
rw [min_eq_right h, map₂_coe, coe_eq]

Result:
case inr
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑b ≤ ↑a
⊢ b =ᶠ[↑φ] fun x => a x ⊓ b x

Proof state:
case inl
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑a ≤ ↑b
⊢ a =ᶠ[↑φ] fun x => a x ⊓ b x

Tactic:
exact h.mono fun i hi => (min_eq_left hi).symm

Result:
no goals

Proof state:
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
⊢ ↑a ⊓ ↑b = map₂ min ↑a ↑b

Tactic:
rcases le_total (a : β*) b with h | h

Result:
case inl
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑a ≤ ↑b
⊢ ↑a ⊓ ↑b = map₂ min ↑a ↑b

case inr
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑b ≤ ↑a
⊢ ↑a ⊓ ↑b = map₂ min ↑a ↑b

Proof state:
case inl
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑a ≤ ↑b
⊢ ↑a ⊓ ↑b = map₂ min ↑a ↑b

Tactic:
rw [min_eq_left h, map₂_coe, coe_eq]

Result:
case inl
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑a ≤ ↑b
⊢ a =ᶠ[↑φ] fun x => a x ⊓ b x
-- Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean
@[simp] lemma smul_bot (a : M) : a • (⊥ : AffineSubspace k V) = ⊥

Proof state:
case h
M : Type u_1
k : Type u_2
V : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : Monoid M
inst✝¹ : DistribMulAction M V
inst✝ : SMulCommClass M k V
a : M
x✝ : V
⊢ x✝ ∈ a • ⊥ ↔ x✝ ∈ ⊥

Tactic:
simp [smul_eq_map, map_bot]

Result:
no goals

Proof state:
M : Type u_1
k : Type u_2
V : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : Monoid M
inst✝¹ : DistribMulAction M V
inst✝ : SMulCommClass M k V
a : M
⊢ a • ⊥ = ⊥

Tactic:
ext

Result:
case h
M : Type u_1
k : Type u_2
V : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : Monoid M
inst✝¹ : DistribMulAction M V
inst✝ : SMulCommClass M k V
a : M
x✝ : V
⊢ x✝ ∈ a • ⊥ ↔ x✝ ∈ ⊥
-- Mathlib/Lean/Meta/CongrTheorems.lean
theorem FastSubsingleton.helim {α β : Sort u} [FastSubsingleton α]
    (h₂ : α = β) (a : α) (b : β) : HEq a b

Proof state:
α β : Sort u
inst✝ : FastSubsingleton α
h₂ : α = β
a : α
b : β
this : Subsingleton α
⊢ HEq a b

Tactic:
exact Subsingleton.helim h₂ a b

Result:
no goals

Proof state:
α β : Sort u
inst✝ : FastSubsingleton α
h₂ : α = β
a : α
b : β
⊢ HEq a b

Tactic:
have : Subsingleton α := FastSubsingleton.inst

Result:
α β : Sort u
inst✝ : FastSubsingleton α
h₂ : α = β
a : α
b : β
this : Subsingleton α
⊢ HEq a b