harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/MetricSpace/Defs.lean
theorem MetricSpace.ext {α : Type*} {m m' : MetricSpace α} (h : m.toDist = m'.toDist) :
    m = m'

Proof state:
α : Type u_3
m m' : MetricSpace α
h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
⊢ m = m'

Tactic:
cases m

Result:
case mk
α : Type u_3
m' : MetricSpace α
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
⊢ mk eq_of_dist_eq_zero✝ = m'

Proof state:
case mk.mk
α : Type u_3
toPseudoMetricSpace✝¹ : PseudoMetricSpace α
eq_of_dist_eq_zero✝¹ : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
⊢ mk eq_of_dist_eq_zero✝¹ = mk eq_of_dist_eq_zero✝

Tactic:
congr

Result:
case mk.mk.e_toPseudoMetricSpace
α : Type u_3
toPseudoMetricSpace✝¹ : PseudoMetricSpace α
eq_of_dist_eq_zero✝¹ : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
⊢ toPseudoMetricSpace✝¹ = toPseudoMetricSpace✝

Proof state:
case mk
α : Type u_3
m' : MetricSpace α
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
⊢ mk eq_of_dist_eq_zero✝ = m'

Tactic:
cases m'

Result:
case mk.mk
α : Type u_3
toPseudoMetricSpace✝¹ : PseudoMetricSpace α
eq_of_dist_eq_zero✝¹ : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
⊢ mk eq_of_dist_eq_zero✝¹ = mk eq_of_dist_eq_zero✝

Proof state:
case mk.mk.e_toPseudoMetricSpace.h
α : Type u_3
toPseudoMetricSpace✝¹ : PseudoMetricSpace α
eq_of_dist_eq_zero✝¹ : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
⊢ PseudoMetricSpace.toDist = PseudoMetricSpace.toDist

Tactic:
assumption

Result:
no goals

Proof state:
case mk.mk.e_toPseudoMetricSpace
α : Type u_3
toPseudoMetricSpace✝¹ : PseudoMetricSpace α
eq_of_dist_eq_zero✝¹ : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
⊢ toPseudoMetricSpace✝¹ = toPseudoMetricSpace✝

Tactic:
ext1

Result:
case mk.mk.e_toPseudoMetricSpace.h
α : Type u_3
toPseudoMetricSpace✝¹ : PseudoMetricSpace α
eq_of_dist_eq_zero✝¹ : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
⊢ PseudoMetricSpace.toDist = PseudoMetricSpace.toDist
-- Mathlib/Data/List/Pairwise.lean
theorem Pairwise.forall (hR : Symmetric R) (hl : l.Pairwise R) :
    ∀ ⦃a⦄, a ∈ l → ∀ ⦃b⦄, b ∈ l → a ≠ b → R a b

Proof state:
α : Type u_1
R : α → α → Prop
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ ∀ ⦃a : α⦄, a ∈ l → ∀ ⦃b : α⦄, b ∈ l → a ≠ b → R a b

Tactic:
apply Pairwise.forall_of_forall

Result:
case H
α : Type u_1
R : α → α → Prop
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ Symmetric fun x y => x ≠ y → R x y

case H₁
α : Type u_1
R : α → α → Prop
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ ∀ (x : α), x ∈ l → x ≠ x → R x x

case H₂
α : Type u_1
R : α → α → Prop
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ Pairwise (fun x y => x ≠ y → R x y) l

Proof state:
case H
α : Type u_1
R : α → α → Prop
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ Symmetric fun x y => x ≠ y → R x y

Tactic:
exact fun a b h hne => hR (h hne.symm)

Result:
no goals

Proof state:
case H₁
α : Type u_1
R : α → α → Prop
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ ∀ (x : α), x ∈ l → x ≠ x → R x x

Tactic:
exact fun _ _ hx => (hx rfl).elim

Result:
no goals

Proof state:
case H₂
α : Type u_1
R : α → α → Prop
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ Pairwise (fun x y => x ≠ y → R x y) l

Tactic:
exact hl.imp (@fun a b h _ => by exact h)

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
l : List α
hR : Symmetric R
hl : Pairwise R l
a b : α
h : R a b
x✝ : a ≠ b
⊢ R a b

Tactic:
exact h

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Presheaf.lean
lemma yonedaEquiv_presheafHom_yoneda_obj (X : C) :
    yonedaEquiv (presheafHom φ (yoneda.obj X)) =
      ((φ.app X).app (F.op.obj (Opposite.op X)) (𝟙 _))

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₁, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁
φ : F ⋙ yoneda ⟶ yoneda ⋙ G
X : C
⊢ yonedaEquiv (presheafHom φ (yoneda.obj X)) =
    (φ.app X).app (F.op.obj (Opposite.op X)) (𝟙 (Opposite.unop (F.op.obj (Opposite.op X))))

Tactic:
simpa using yonedaEquiv_ι_presheafHom φ (yoneda.obj X) (𝟙 _)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean
theorem finite_integral_one_add_norm {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r) :
    (∫⁻ x : E, ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) ∂μ) < ∞

Proof state:
case calc_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → μ {a | t ≤ (1 + ‖a‖) ^ (-r)} = μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := μ (Metric.ball 0 1)
h_int' : ∀ t ∈ Ioc 0 1, f t = ENNReal.ofReal ((t ^ (-r⁻¹) - 1) ^ finrank ℝ E) * mB
⊢ ∫⁻ (t : ℝ) in Ioc 0 1, f t < ⊤

Tactic:
rw [setLIntegral_congr_fun measurableSet_Ioc (ae_of_all _ h_int'),
  lintegral_mul_const' _ _ measure_ball_lt_top.ne]

Result:
case calc_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → μ {a | t ≤ (1 + ‖a‖) ^ (-r)} = μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := μ (Metric.ball 0 1)
h_int' : ∀ t ∈ Ioc 0 1, f t = ENNReal.ofReal ((t ^ (-r⁻¹) - 1) ^ finrank ℝ E) * mB
⊢ (∫⁻ (a : ℝ) in Ioc 0 1, ENNReal.ofReal ((a ^ (-r⁻¹) - 1) ^ finrank ℝ E) ∂volume) * μ (Metric.ball 0 1) < ⊤

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → μ {a | t ≤ (1 + ‖a‖) ^ (-r)} = μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
⊢ ∫⁻ (x : ℝ) in Ioi 0, μ (Metric.closedBall 0 (x ^ (-r⁻¹) - 1)) ∂volume < ⊤

Tactic:
set f := fun t : ℝ ↦ μ (Metric.closedBall (0 : E) (t ^ (-r⁻¹) - 1))

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → μ {a | t ≤ (1 + ‖a‖) ^ (-r)} = μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
⊢ lintegral (volume.restrict (Ioi 0)) f < ⊤

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
⊢ Measurable fun ω => (1 + ‖ω‖) ^ (-r)

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Algebra/Prime/Lemmas.lean
theorem irreducible_mul_iff {a b : M} :
    Irreducible (a * b) ↔ Irreducible a ∧ IsUnit b ∨ Irreducible b ∧ IsUnit a

Proof state:
case mp.refine_2
M : Type u_1
inst✝ : Monoid M
a b : M
h : Irreducible (a * b)
h' : IsUnit a
⊢ Irreducible b

Tactic:
rwa [irreducible_isUnit_mul h'] at h

Result:
no goals

Proof state:
case mp
M : Type u_1
inst✝ : Monoid M
a b : M
⊢ Irreducible (a * b) → Irreducible a ∧ IsUnit b ∨ Irreducible b ∧ IsUnit a

Tactic:
refine fun h => Or.imp (fun h' => ⟨?_, h'⟩) (fun h' => ⟨?_, h'⟩) (h.isUnit_or_isUnit rfl).symm

Result:
case mp.refine_1
M : Type u_1
inst✝ : Monoid M
a b : M
h : Irreducible (a * b)
h' : IsUnit b
⊢ Irreducible a

case mp.refine_2
M : Type u_1
inst✝ : Monoid M
a b : M
h : Irreducible (a * b)
h' : IsUnit a
⊢ Irreducible b

Proof state:
case mpr.inl.intro
M : Type u_1
inst✝ : Monoid M
a b : M
ha : Irreducible a
hb : IsUnit b
⊢ Irreducible (a * b)

Tactic:
rwa [irreducible_mul_isUnit hb]

Result:
no goals

Proof state:
case mpr.inr.intro
M : Type u_1
inst✝ : Monoid M
a b : M
hb : Irreducible b
ha : IsUnit a
⊢ Irreducible (a * b)

Tactic:
rwa [irreducible_isUnit_mul ha]

Result:
no goals

Proof state:
case mpr
M : Type u_1
inst✝ : Monoid M
a b : M
⊢ Irreducible a ∧ IsUnit b ∨ Irreducible b ∧ IsUnit a → Irreducible (a * b)

Tactic:
rintro (⟨ha, hb⟩ | ⟨hb, ha⟩)

Result:
case mpr.inl.intro
M : Type u_1
inst✝ : Monoid M
a b : M
ha : Irreducible a
hb : IsUnit b
⊢ Irreducible (a * b)

case mpr.inr.intro
M : Type u_1
inst✝ : Monoid M
a b : M
hb : Irreducible b
ha : IsUnit a
⊢ Irreducible (a * b)

Proof state:
case mp.refine_1
M : Type u_1
inst✝ : Monoid M
a b : M
h : Irreducible (a * b)
h' : IsUnit b
⊢ Irreducible a

Tactic:
rwa [irreducible_mul_isUnit h'] at h

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
a b : M
⊢ Irreducible (a * b) ↔ Irreducible a ∧ IsUnit b ∨ Irreducible b ∧ IsUnit a

Tactic:
constructor

Result:
case mp
M : Type u_1
inst✝ : Monoid M
a b : M
⊢ Irreducible (a * b) → Irreducible a ∧ IsUnit b ∨ Irreducible b ∧ IsUnit a

case mpr
M : Type u_1
inst✝ : Monoid M
a b : M
⊢ Irreducible a ∧ IsUnit b ∨ Irreducible b ∧ IsUnit a → Irreducible (a * b)
-- Mathlib/Data/Fin/Parity.lean
lemma even_iff_of_even {n : ℕ} (hn : Even n) {k : Fin n} : Even k ↔ Even k.val

Proof state:
case intro
n : ℕ
k : Fin (n + n)
⊢ Even k → Even ↑k

Tactic:
rintro ⟨l, rfl⟩

Result:
case intro.intro
n : ℕ
l : Fin (n + n)
⊢ Even ↑(l + l)

Proof state:
case intro
n : ℕ
k : Fin (n + n)
⊢ Even k ↔ Even ↑k

Tactic:
refine ⟨?_, even_of_val⟩

Result:
case intro
n : ℕ
k : Fin (n + n)
⊢ Even k → Even ↑k

Proof state:
case intro.intro
n : ℕ
l : Fin (n + n)
⊢ Even (if n + n ≤ ↑l + ↑l then ↑l + ↑l - (n + n) else ↑l + ↑l)

Tactic:
split_ifs with h <;> simp [Nat.even_sub, *]

Result:
no goals

Proof state:
n : ℕ
hn : Even n
k : Fin n
⊢ Even k ↔ Even ↑k

Tactic:
rcases hn with ⟨n, rfl⟩

Result:
case intro
n : ℕ
k : Fin (n + n)
⊢ Even k ↔ Even ↑k

Proof state:
case intro.intro
n : ℕ
l : Fin (n + n)
⊢ Even ↑(l + l)

Tactic:
rw [val_add_eq_ite]

Result:
case intro.intro
n : ℕ
l : Fin (n + n)
⊢ Even (if n + n ≤ ↑l + ↑l then ↑l + ↑l - (n + n) else ↑l + ↑l)
-- Mathlib/Topology/Category/Stonean/Basic.lean
@[simp, reassoc]
lemma lift_lifts {X Y : CompHaus} {Z : Stonean} (e : Z.compHaus ⟶ Y) (f : X ⟶ Y) [Epi f] :
    lift e f ≫ f = e

Proof state:
X Y : CompHaus
Z : Stonean
e : Z.compHaus ⟶ Y
f : X ⟶ Y
inst✝ : Epi f
⊢ lift e f ≫ f = e

Tactic:
simp [lift]

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem Subalgebra.restrictScalars_adjoin {s : Set A} :
    (adjoin S s).restrictScalars R = (IsScalarTower.toAlgHom R S A).range ⊔ adjoin R s

Proof state:
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
⊢ Subalgebra.restrictScalars R (adjoin S s) = (IsScalarTower.toAlgHom R S A).range ⊔ adjoin R s

Tactic:
refine le_antisymm (fun _ hx ↦ adjoin_induction
  (fun x hx ↦ le_sup_right (α := Subalgebra R A) (subset_adjoin hx))
  (fun x ↦ le_sup_left (α := Subalgebra R A) ⟨x, rfl⟩)
  (fun _ _ _ _ ↦ add_mem) (fun _ _ _ _ ↦ mul_mem) <|
  (Subalgebra.mem_restrictScalars _).mp hx) (sup_le ?_ <| adjoin_le subset_adjoin)

Result:
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
⊢ (IsScalarTower.toAlgHom R S A).range ≤ Subalgebra.restrictScalars R (adjoin S s)

Proof state:
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
⊢ (IsScalarTower.toAlgHom R S A).range ≤ Subalgebra.restrictScalars R (adjoin S s)

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case intro
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
x : S
⊢ (IsScalarTower.toAlgHom R S A).toRingHom x ∈ Subalgebra.restrictScalars R (adjoin S s)

Proof state:
case intro
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
x : S
⊢ (IsScalarTower.toAlgHom R S A).toRingHom x ∈ Subalgebra.restrictScalars R (adjoin S s)

Tactic:
exact algebraMap_mem (adjoin S s) x

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
private lemma isBigO_one_aux :
    IsBigO atTop (fun t : ℝ ↦ (1 - rexp (-π * t))⁻¹) (fun _ ↦ (1 : ℝ))

Proof state:
⊢ Tendsto (fun x => rexp (-π * x)) atTop (𝓝 0)

Tactic:
simpa only [neg_mul, tendsto_exp_comp_nhds_zero, tendsto_neg_atBot_iff]
  using tendsto_id.const_mul_atTop pi_pos

Result:
no goals

Proof state:
⊢ (fun t => (1 - rexp (-π * t))⁻¹) =O[atTop] fun x => 1

Tactic:
refine ((Tendsto.const_sub _ ?_).inv₀ (by norm_num)).isBigO_one ℝ (c := ((1 - 0)⁻¹ : ℝ))

Result:
⊢ Tendsto (fun x => rexp (-π * x)) atTop (𝓝 0)

Proof state:
⊢ 1 - 0 ≠ 0

Tactic:
norm_num

Result:
no goals
-- Mathlib/RingTheory/FiniteType.lean
theorem of'_mem_span [Nontrivial R] {m : M} {S : Set M} :
    of' R M m ∈ span R (of' R M '' S) ↔ m ∈ S

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
⊢ of' R M m ∈ span R (of' R M '' S) ↔ m ∈ S

Tactic:
refine ⟨fun h => ?_, fun h => Submodule.subset_span <| Set.mem_image_of_mem (of R M) h⟩

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : of' R M m ∈ span R (of' R M '' S)
⊢ m ∈ S

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : ↑{m} ⊆ S
⊢ m ∈ S

Tactic:
simpa using h

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : of' R M m ∈ span R (of' R M '' S)
⊢ m ∈ S

Tactic:
erw [of', ← Finsupp.supported_eq_span_single, Finsupp.mem_supported,
  Finsupp.support_single_ne_zero _ (one_ne_zero' R)] at h

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : ↑{m} ⊆ S
⊢ m ∈ S
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_eq_some_getValueD [BEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β}
    (h : containsKey a l = true) : getValue? a l = some (getValueD a l fallback)

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
a : α
fallback : β
h : containsKey a l = true
⊢ getValue? a l = some (getValueD a l fallback)

Tactic:
rw [getValue?_eq_some_getValue h, getValue_eq_getValueD]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem affineIndependent_iff_indicator_eq_of_affineCombination_eq (p : ι → P) :
    AffineIndependent k p ↔
      ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
        ∑ i ∈ s1, w1 i = 1 →
          ∑ i ∈ s2, w2 i = 1 →
            s1.affineCombination k p w1 = s2.affineCombination k p w2 →
              Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2

Proof state:
case neg
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
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1, w1 i = 1
hw2 : ∑ i ∈ s2, w2 i = 1
heq : (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2
i : ι
hi : i ∉ ↑s1 ∪ ↑s2
h₁ : (↑s1).indicator w1 i = 0
⊢ (↑s1).indicator w1 i = (↑s2).indicator w2 i

Tactic:
have h₂ : Set.indicator (↑s2) w2 i = 0 := by
  simp only [Set.indicator, Finset.mem_coe, ite_eq_right_iff]
  intro h
  by_contra
  exact (mt (@Set.mem_union_right _ i ↑s2 ↑s1) hi) h

Result:
case neg
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
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1, w1 i = 1
hw2 : ∑ i ∈ s2, w2 i = 1
heq : (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2
i : ι
hi : i ∉ ↑s1 ∪ ↑s2
h₁ : (↑s1).indicator w1 i = 0
h₂ : (↑s2).indicator w2 i = 0
⊢ (↑s1).indicator w1 i = (↑s2).indicator w2 i
-- Mathlib/LinearAlgebra/Projectivization/Basic.lean
theorem mk_eq_mk_iff' (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) :
    mk K v hv = mk K w hw ↔ ∃ a : K, a • w = v

Proof state:
case mpr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) → ∃ a, a • w = v

Tactic:
rintro ⟨a, ha⟩

Result:
case mpr.intro
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
⊢ ∃ a, a • w = v

Proof state:
case mpr.intro
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
c : a = 0
⊢ 0 = v

Tactic:
rwa [c, zero_smul] at ha

Result:
no goals

Proof state:
case mp
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) → ∃ a, a • w = v

Tactic:
rintro ⟨a, ha⟩

Result:
case mp.intro
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : Kˣ
ha : a • w = v
⊢ ∃ a, a • w = v

Proof state:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) ↔ ∃ a, a • w = v

Tactic:
constructor

Result:
case mp
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) → ∃ a, a • w = v

case mpr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) → ∃ a, a • w = v

Proof state:
case mp.intro
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : Kˣ
ha : a • w = v
⊢ ∃ a, a • w = v

Tactic:
exact ⟨a, ha⟩

Result:
no goals

Proof state:
case mpr.intro
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
⊢ ∃ a, a • w = v

Tactic:
refine ⟨Units.mk0 a fun c => hv.symm ?_, ha⟩

Result:
case mpr.intro
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
c : a = 0
⊢ 0 = v

Proof state:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ mk K v hv = mk K w hw ↔ ∃ a, a • w = v

Tactic:
rw [mk_eq_mk_iff K v w hv hw]

Result:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) ↔ ∃ a, a • w = v
-- Mathlib/RingTheory/Trace/Defs.lean
theorem trace_prod [Module.Free R S] [Module.Free R T] [Module.Finite R S] [Module.Finite R T] :
    trace R (S × T) = (trace R S).coprod (trace R T) :=
  LinearMap.ext fun p => by rw [coprod_apply, trace_prod_apply]

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Free R S
inst✝² : Free R T
inst✝¹ : Module.Finite R S
inst✝ : Module.Finite R T
p : S × T
⊢ (trace R (S × T)) p = ((trace R S).coprod (trace R T)) p

Tactic:
rw [coprod_apply, trace_prod_apply]

Result:
no goals
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_eq_prod {α : Type*} [CommMonoid α] (s : Multiset α) :
    (noncommProd s fun _ _ _ _ _ => Commute.all _ _) = prod s

Proof state:
case h
α : Type u_6
inst✝ : CommMonoid α
a✝ : List α
⊢ noncommProd ⟦a✝⟧ ⋯ = prod ⟦a✝⟧

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_6
inst✝ : CommMonoid α
s : Multiset α
⊢ s.noncommProd ⋯ = s.prod

Tactic:
induction s using Quotient.inductionOn

Result:
case h
α : Type u_6
inst✝ : CommMonoid α
a✝ : List α
⊢ noncommProd ⟦a✝⟧ ⋯ = prod ⟦a✝⟧