harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem dist_triangle4_left (x₁ y₁ x₂ y₂ : α) :
    dist x₂ y₂ ≤ dist x₁ y₁ + (dist x₁ x₂ + dist y₁ y₂)

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
⊢ dist x₂ y₂ ≤ dist x₂ x₁ + dist x₁ y₁ + dist y₁ y₂

Tactic:
apply dist_triangle4

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
⊢ dist x₂ y₂ ≤ dist x₁ y₁ + (dist x₁ x₂ + dist y₁ y₂)

Tactic:
rw [add_left_comm, dist_comm x₁, ← add_assoc]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
⊢ dist x₂ y₂ ≤ dist x₂ x₁ + dist x₁ y₁ + dist y₁ y₂
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem sInf_toSubmodule (S : Set (Subalgebra R A)) :
    Subalgebra.toSubmodule (sInf S) = sInf (Subalgebra.toSubmodule '' S) :=
  SetLike.coe_injective <| by simp

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
⊢ ↑(Subalgebra.toSubmodule (sInf S)) = ↑(sInf (⇑Subalgebra.toSubmodule '' S))

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem Ultrafilter.le_nhds_lim [CompactSpace X] (F : Ultrafilter X) : ↑F ≤ 𝓝 F.lim

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
F : Ultrafilter X
⊢ ↑F ≤ 𝓟 univ

Tactic:
simp

Result:
no goals

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
F : Ultrafilter X
⊢ ↑F ≤ 𝓝 F.lim

Tactic:
rcases isCompact_univ.ultrafilter_le_nhds F (by simp) with ⟨x, -, h⟩

Result:
case intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
F : Ultrafilter X
x : X
h : ↑F ≤ 𝓝 x
⊢ ↑F ≤ 𝓝 F.lim

Proof state:
case intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
F : Ultrafilter X
x : X
h : ↑F ≤ 𝓝 x
⊢ ↑F ≤ 𝓝 F.lim

Tactic:
exact le_nhds_lim ⟨x, h⟩

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem HasMFDerivAt.mdifferentiableAt (h : HasMFDerivAt I I' f x f') :
    MDifferentiableAt I I' f x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivAt I I' f x f'
⊢ ContinuousAt f x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range ↑I) (↑(extChartAt I x) x)

Tactic:
exact ⟨h.1, ⟨f', h.2⟩⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivAt I I' f x f'
⊢ MDifferentiableAt I I' f x

Tactic:
rw [mdifferentiableAt_iff]

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivAt I I' f x f'
⊢ ContinuousAt f x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range ↑I) (↑(extChartAt I x) x)
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem mk_one_mul_one_sub_eq_one : (mk 1 : S⟦X⟧) * (1 - X) = 1

Proof state:
S : Type u_1
inst✝ : CommRing S
n : ℕ
⊢ (coeff S n) ((1 - X) * mk 1) = (coeff S n) 1

Tactic:
cases n with
| zero => simp
| succ n => simp [sub_mul]

Result:
no goals

Proof state:
S : Type u_1
inst✝ : CommRing S
⊢ ∀ (n : ℕ), (coeff S n) ((1 - X) * mk 1) = (coeff S n) 1

Tactic:
intro n

Result:
S : Type u_1
inst✝ : CommRing S
n : ℕ
⊢ (coeff S n) ((1 - X) * mk 1) = (coeff S n) 1

Proof state:
case zero
S : Type u_1
inst✝ : CommRing S
⊢ (coeff S 0) ((1 - X) * mk 1) = (coeff S 0) 1

Tactic:
simp

Result:
no goals

Proof state:
S : Type u_1
inst✝ : CommRing S
⊢ mk 1 * (1 - X) = 1

Tactic:
rw [mul_comm, PowerSeries.ext_iff]

Result:
S : Type u_1
inst✝ : CommRing S
⊢ ∀ (n : ℕ), (coeff S n) ((1 - X) * mk 1) = (coeff S n) 1

Proof state:
case succ
S : Type u_1
inst✝ : CommRing S
n : ℕ
⊢ (coeff S (n + 1)) ((1 - X) * mk 1) = (coeff S (n + 1)) 1

Tactic:
simp [sub_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Core.lean
theorem Thunk.sizeOf_eq [SizeOf α] (a : Thunk α) : sizeOf a = 1 + sizeOf a.get

Proof state:
case mk
α : Type u_1
inst✝ : SizeOf α
fn✝ : Unit → α
⊢ sizeOf { fn := fn✝ } = 1 + sizeOf { fn := fn✝ }.get

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : SizeOf α
a : Thunk α
⊢ sizeOf a = 1 + sizeOf a.get

Tactic:
cases a

Result:
case mk
α : Type u_1
inst✝ : SizeOf α
fn✝ : Unit → α
⊢ sizeOf { fn := fn✝ } = 1 + sizeOf { fn := fn✝ }.get
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head?_isSome : l.head?.isSome ↔ l ≠ []

Proof state:
α✝ : Type u_1
l : List α✝
⊢ l.head?.isSome = true ↔ l ≠ []

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[simp]
lemma lift_comp_fst_snd {X Y Z : C} (f : X ⟶ Y ⊗ Z) :
    lift (f ≫ fst _ _) (f ≫ snd _ _) = f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y Z : C
f : X ⟶ Y ⊗ Z
⊢ lift (f ≫ fst Y Z) (f ≫ snd Y Z) = f

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/NumberTheory/FermatPsp.lean
theorem b_id_helper {a b : ℕ} (ha : 2 ≤ a) (hb : 2 < b) : 2 ≤ (a ^ b + 1) / (a + 1)

Proof state:
case a
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ Nat.mul 2 a + 1 ≤ a ^ b

Tactic:
calc
  2 * a + 1 ≤ a ^ 2 * a := by nlinarith
  _ = a ^ 3 := by rw [Nat.pow_succ a 2]
  _ ≤ a ^ b := pow_right_mono₀ (Nat.le_of_succ_le ha) hb

Result:
no goals

Proof state:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ a ^ 2 * a = a ^ 3

Tactic:
rw [Nat.pow_succ a 2]

Result:
no goals

Proof state:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ 2 * a + 1 ≤ a ^ 2 * a

Tactic:
nlinarith

Result:
no goals

Proof state:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ 2 * a.succ ≤ a ^ b + 1

Tactic:
apply Nat.succ_le_succ

Result:
case a
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ Nat.mul 2 a + 1 ≤ a ^ b

Proof state:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ 2 ≤ (a ^ b + 1) / (a + 1)

Tactic:
rw [Nat.le_div_iff_mul_le (Nat.zero_lt_succ _)]

Result:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ 2 * a.succ ≤ a ^ b + 1
-- Mathlib/NumberTheory/LSeries/Linearity.lean
lemma LSeries.term_neg_apply (f : ℕ → ℂ) (s : ℂ) (n : ℕ) : term (-f) s n = -term f s n

Proof state:
f : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term (-f) s n = -term f s n

Tactic:
simp [term_neg]

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/Units.lean
theorem inverse_add (x : Rˣ) :
    ∀ᶠ t in 𝓝 0, inverse ((x : R) + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
t : R
ht : dist t 0 < ‖↑x⁻¹‖⁻¹
⊢ inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹

Tactic:
rw [dist_zero_right] at ht

Result:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
t : R
ht : ‖t‖ < ‖↑x⁻¹‖⁻¹
⊢ inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
t : R
ht : ‖t‖ < ‖↑x⁻¹‖⁻¹
⊢ inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹

Tactic:
rw [← x.val_add t ht, inverse_unit, Units.add, Units.copy_eq, mul_inv_rev, Units.val_mul,
  ← inverse_unit, Units.val_oneSub, sub_neg_eq_add]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
⊢ ‖↑x⁻¹‖⁻¹ > 0

Tactic:
cancel_denoms

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
⊢ ∀ᶠ (t : R) in 𝓝 0, inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹

Tactic:
rw [Metric.eventually_nhds_iff]

Result:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
⊢ ∃ ε > 0, ∀ ⦃y : R⦄, dist y 0 < ε → inverse (↑x + y) = inverse (1 + ↑x⁻¹ * y) * ↑x⁻¹

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
⊢ ∃ ε > 0, ∀ ⦃y : R⦄, dist y 0 < ε → inverse (↑x + y) = inverse (1 + ↑x⁻¹ * y) * ↑x⁻¹

Tactic:
refine ⟨‖(↑x⁻¹ : R)‖⁻¹, by cancel_denoms, fun t ht ↦ ?_⟩

Result:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
t : R
ht : dist t 0 < ‖↑x⁻¹‖⁻¹
⊢ inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
⊢ ∀ᶠ (t : R) in 𝓝 0, inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹

Tactic:
nontriviality R

Result:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
⊢ ∀ᶠ (t : R) in 𝓝 0, inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem weightedHomogeneousComponent_finsupp :
    (Function.support fun m => weightedHomogeneousComponent w m φ).Finite

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
m : M
hm : m ∈ Function.support fun m => (weightedHomogeneousComponent w m) φ
⊢ m ∈ (fun d => (weight w) d) '' ↑φ.support

Tactic:
by_contra hm'

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
m : M
hm : m ∈ Function.support fun m => (weightedHomogeneousComponent w m) φ
hm' : m ∉ (fun d => (weight w) d) '' ↑φ.support
⊢ False

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
⊢ (Function.support fun m => (weightedHomogeneousComponent w m) φ).Finite

Tactic:
apply ((fun d : σ →₀ ℕ => (weight w) d) '' (φ.support : Set (σ →₀ ℕ))).toFinite.subset

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
⊢ (Function.support fun m => (weightedHomogeneousComponent w m) φ) ⊆ (fun d => (weight w) d) '' ↑φ.support

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
m : M
hm : m ∈ Function.support fun m => (weightedHomogeneousComponent w m) φ
hm' : m ∉ (fun d => (weight w) d) '' ↑φ.support
⊢ False

Tactic:
apply hm (weightedHomogeneousComponent_eq_zero' m φ _)

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
m : M
hm : m ∈ Function.support fun m => (weightedHomogeneousComponent w m) φ
hm' : m ∉ (fun d => (weight w) d) '' ↑φ.support
⊢ ∀ d ∈ φ.support, (weight w) d ≠ m

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
⊢ (Function.support fun m => (weightedHomogeneousComponent w m) φ) ⊆ (fun d => (weight w) d) '' ↑φ.support

Tactic:
intro m hm

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
m : M
hm : m ∈ Function.support fun m => (weightedHomogeneousComponent w m) φ
⊢ m ∈ (fun d => (weight w) d) '' ↑φ.support

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
m : M
hm : m ∈ Function.support fun m => (weightedHomogeneousComponent w m) φ
hm' : m ∉ (fun d => (weight w) d) '' ↑φ.support
⊢ ∀ d ∈ φ.support, (weight w) d ≠ m

Tactic:
simpa only [Set.mem_image, not_exists, not_and] using hm'

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma pow_eq_neg_one_iff : a ^ n = -1 ↔ a = -1 ∧ Odd n

Proof state:
R : Type u_2
inst✝ : LinearOrderedRing R
a : R
n : ℕ
⊢ a ^ n = -1 ↔ a = -1 ∧ Odd n

Tactic:
simpa using pow_eq_neg_pow_iff (R := R) one_ne_zero

Result:
no goals
-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem compatible_iff_sieveCompatible (x : FamilyOfElements P (S : Presieve X)) :
    x.Compatible ↔ x.SieveCompatible

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
⊢ x.Compatible ↔ x.SieveCompatible

Tactic:
constructor

Result:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
⊢ x.Compatible → x.SieveCompatible

case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
⊢ x.SieveCompatible → x.Compatible

Proof state:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
⊢ x.Compatible → x.SieveCompatible

Tactic:
intro h Y Z f g hf

Result:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
h : x.Compatible
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
⊢ x (g ≫ f) ⋯ = P.map g.op (x f hf)

Proof state:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
⊢ x.SieveCompatible → x.Compatible

Tactic:
intro h Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ k

Result:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : S.arrows f₁
h₂ : S.arrows f₂
k : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map g₁.op (x f₁ h₁) = P.map g₂.op (x f₂ h₂)

Proof state:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : S.arrows f₁
h₂ : S.arrows f₂
k : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ x (g₁ ≫ f₁) ⋯ = x (g₂ ≫ f₂) ⋯

Tactic:
congr

Result:
no goals

Proof state:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
h : x.Compatible
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
⊢ x (g ≫ f) ⋯ = P.map g.op (x f hf)

Tactic:
simpa using h (𝟙 _) g (S.downward_closed hf g) hf (id_comp _)

Result:
no goals

Proof state:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : S.arrows f₁
h₂ : S.arrows f₂
k : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map g₁.op (x f₁ h₁) = P.map g₂.op (x f₂ h₂)

Tactic:
simp_rw [← h f₁ g₁ h₁, ← h f₂ g₂ h₂]

Result:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : S.arrows f₁
h₂ : S.arrows f₂
k : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ x (g₁ ≫ f₁) ⋯ = x (g₂ ≫ f₂) ⋯
-- Mathlib/Algebra/Order/Sub/WithTop.lean
lemma sub_ne_top_iff {a b : WithTop α} : a - b ≠ ⊤ ↔ a ≠ ⊤ ∨ b = ⊤

Proof state:
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a b : WithTop α
⊢ a - b ≠ ⊤ ↔ a ≠ ⊤ ∨ b = ⊤

Tactic:
simp [or_iff_not_imp_left]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem submonoid_closure_range_simple : Submonoid.closure (range cs.simple) = ⊤

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
this : Set.range cs.simple = Set.range cs.simple ∪ (Set.range cs.simple)⁻¹
⊢ Submonoid.closure (Set.range cs.simple) = ⊤

Tactic:
rw [this, ← Subgroup.closure_toSubmonoid, subgroup_closure_range_simple, Subgroup.top_toSubmonoid]

Result:
no goals

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ Submonoid.closure (Set.range cs.simple) = ⊤

Tactic:
have : range cs.simple = range cs.simple ∪ (range cs.simple)⁻¹ := by
  simp_rw [inv_range, inv_simple, union_self]

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
this : Set.range cs.simple = Set.range cs.simple ∪ (Set.range cs.simple)⁻¹
⊢ Submonoid.closure (Set.range cs.simple) = ⊤

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ Set.range cs.simple = Set.range cs.simple ∪ (Set.range cs.simple)⁻¹

Tactic:
simp_rw [inv_range, inv_simple, union_self]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem BijOn.exists_extend_of_subset {t' : Set β} (h : BijOn f s t) (hss₁ : s ⊆ s₁) (htt' : t ⊆ t')
    (ht' : SurjOn f s₁ t') : ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ Set.BijOn f s' t'

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'

Tactic:
refine ⟨s ∪ r, subset_union_left, ?_, ?_, ?_, fun y hyt' ↦ ?_⟩

Result:
case intro.intro.refine_1
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ s ∪ r ⊆ s₁

case intro.intro.refine_2
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ MapsTo f (s ∪ r) t'

case intro.intro.refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ InjOn f (s ∪ r)

case intro.intro.refine_4
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
y : β
hyt' : y ∈ t'
⊢ y ∈ f '' (s ∪ r)
-- Mathlib/Algebra/Order/Sub/Basic.lean
theorem tsub_min : a - min a b = a - b

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

Tactic:
rcases le_total a b with h | h

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

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

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

Tactic:
rw [min_eq_right h]

Result:
no goals

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

Tactic:
rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem add_comm : ∀ (n m : Nat), n + m = m + n
  | n, 0   => Eq.symm (Nat.zero_add n)
  | n, m+1 => by
    have : succ (n + m) = succ (m + n)

Proof state:
n m : Nat
this : (n + m).succ = (m + n).succ
⊢ n + (m + 1) = (m + n).succ

Tactic:
apply this

Result:
no goals

Proof state:
n m : Nat
this : (n + m).succ = (m + n).succ
⊢ n + (m + 1) = m + 1 + n

Tactic:
rw [succ_add m n]

Result:
n m : Nat
this : (n + m).succ = (m + n).succ
⊢ n + (m + 1) = (m + n).succ

Proof state:
n m : Nat
⊢ n + (m + 1) = m + 1 + n

Tactic:
have : succ (n + m) = succ (m + n) := by apply congrArg; apply Nat.add_comm

Result:
n m : Nat
this : (n + m).succ = (m + n).succ
⊢ n + (m + 1) = m + 1 + n

Proof state:
case h
n m : Nat
⊢ n + m = m + n

Tactic:
apply Nat.add_comm

Result:
no goals

Proof state:
n m : Nat
⊢ (n + m).succ = (m + n).succ

Tactic:
apply congrArg

Result:
case h
n m : Nat
⊢ n + m = m + n
-- Mathlib/RingTheory/SurjectiveOnStalks.lean
/--
`R_p →+* S_q` is surjective if and only if
every `x : S` is of the form `f x / f r` for some `f r ∉ q`.
This is useful when proving `SurjectiveOnStalks`.
-/
lemma surjective_localRingHom_iff (P : Ideal S) [P.IsPrime] :
    Function.Surjective (Localization.localRingHom _ P f rfl) ↔
      ∀ s : S, ∃ x r : R, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x

Proof state:
case mp.intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
y : S
a : R
t : ↥(Ideal.comap f P).primeCompl
c : ↥P.primeCompl
hc : ↑c * f a = ↑c * f ↑t * y
⊢ ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * y = c * f x

Tactic:
exact ⟨_, _, _, c.2, t.2, hc.symm⟩

Result:
no goals

Proof state:
case mpr
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
⊢ ∃ a, (Localization.localRingHom (Ideal.comap f P) P f ⋯) a = Localization.mk (y, ⟨t, h⟩).1 (y, ⟨t, h⟩).2

Tactic:
simp only

Result:
case mpr
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
⊢ ∃ a, (Localization.localRingHom (Ideal.comap f P) P f ⋯) a = Localization.mk y ⟨t, h⟩

Proof state:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ yc * yt * (t * (f yx * f ts)) = yc * yt * (f ys * f tx * y)

Tactic:
convert congr($(ey.symm) * $(et)) using 1 <;> ring

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/Isometry.lean
theorem range_eq_univ (e : P ≃ᵃⁱ[𝕜] P₂) : Set.range e = Set.univ

Proof state:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
e : P ≃ᵃⁱ[𝕜] P₂
⊢ range ⇑e.toIsometryEquiv = univ

Tactic:
exact IsometryEquiv.range_eq_univ _

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
e : P ≃ᵃⁱ[𝕜] P₂
⊢ range ⇑e = univ

Tactic:
rw [← coe_toIsometryEquiv]

Result:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
e : P ≃ᵃⁱ[𝕜] P₂
⊢ range ⇑e.toIsometryEquiv = univ