harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem opow_le_opow_left {a b : Ordinal} (c : Ordinal) (ab : a ≤ b) : a ^ c ≤ b ^ c

Proof state:
case pos
a b c : Ordinal.{u_1}
ab : a ≤ b
a0 : a = 0
⊢ a ^ c ≤ b ^ c

Tactic:
subst a

Result:
case pos
b c : Ordinal.{u_1}
ab : 0 ≤ b
⊢ 0 ^ c ≤ b ^ c

Proof state:
case neg
a b c : Ordinal.{u_1}
ab : a ≤ b
a0 : ¬a = 0
⊢ a ^ c ≤ b ^ c

Tactic:
induction c using limitRecOn with
| H₁ => simp only [opow_zero, le_refl]
| H₂ c IH =>
  simpa only [opow_succ] using mul_le_mul' IH ab
| H₃ c l IH =>
  exact
    (opow_le_of_limit a0 l).2 fun b' h =>
      (IH _ h).trans (opow_le_opow_right ((Ordinal.pos_iff_ne_zero.2 a0).trans_le ab) h.le)

Result:
no goals

Proof state:
case neg.H₃
a b : Ordinal.{u_1}
ab : a ≤ b
a0 : ¬a = 0
c : Ordinal.{u_1}
l : c.IsLimit
IH : ∀ o' < c, a ^ o' ≤ b ^ o'
⊢ a ^ c ≤ b ^ c

Tactic:
exact
  (opow_le_of_limit a0 l).2 fun b' h =>
    (IH _ h).trans (opow_le_opow_right ((Ordinal.pos_iff_ne_zero.2 a0).trans_le ab) h.le)

Result:
no goals

Proof state:
a b c : Ordinal.{u_1}
ab : a ≤ b
⊢ a ^ c ≤ b ^ c

Tactic:
by_cases a0 : a = 0

Result:
case pos
a b c : Ordinal.{u_1}
ab : a ≤ b
a0 : a = 0
⊢ a ^ c ≤ b ^ c

case neg
a b c : Ordinal.{u_1}
ab : a ≤ b
a0 : ¬a = 0
⊢ a ^ c ≤ b ^ c

Proof state:
case pos
b : Ordinal.{u_1}
ab : 0 ≤ b
⊢ 0 ^ 0 ≤ b ^ 0

Tactic:
simp only [opow_zero, le_refl]

Result:
no goals

Proof state:
case neg.H₂
a b : Ordinal.{u_1}
ab : a ≤ b
a0 : ¬a = 0
c : Ordinal.{u_1}
IH : a ^ c ≤ b ^ c
⊢ a ^ succ c ≤ b ^ succ c

Tactic:
simpa only [opow_succ] using mul_le_mul' IH ab

Result:
no goals

Proof state:
case pos
b c : Ordinal.{u_1}
ab : 0 ≤ b
c0 : c = 0
⊢ 0 ^ c ≤ b ^ c

Tactic:
subst c

Result:
case pos
b : Ordinal.{u_1}
ab : 0 ≤ b
⊢ 0 ^ 0 ≤ b ^ 0

Proof state:
case neg
b c : Ordinal.{u_1}
ab : 0 ≤ b
c0 : ¬c = 0
⊢ 0 ^ c ≤ b ^ c

Tactic:
simp only [zero_opow c0, Ordinal.zero_le]

Result:
no goals

Proof state:
case pos
b c : Ordinal.{u_1}
ab : 0 ≤ b
⊢ 0 ^ c ≤ b ^ c

Tactic:
by_cases c0 : c = 0

Result:
case pos
b c : Ordinal.{u_1}
ab : 0 ≤ b
c0 : c = 0
⊢ 0 ^ c ≤ b ^ c

case neg
b c : Ordinal.{u_1}
ab : 0 ≤ b
c0 : ¬c = 0
⊢ 0 ^ c ≤ b ^ c

Proof state:
case neg.H₁
a b : Ordinal.{u_1}
ab : a ≤ b
a0 : ¬a = 0
⊢ a ^ 0 ≤ b ^ 0

Tactic:
simp only [opow_zero, le_refl]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/FourFunctions.lean
/-- The `n = 1` case of the Ahlswede-Daykin inequality. Note that we can't just expand everything
out and bound termwise since `c₀ * d₁` appears twice on the RHS of the assumptions while `c₁ * d₀`
does not appear. -/
private lemma ineq [ExistsAddOfLE β] {a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β}
    (ha₀ : 0 ≤ a₀) (ha₁ : 0 ≤ a₁) (hb₀ : 0 ≤ b₀) (hb₁ : 0 ≤ b₁)
    (hc₀ : 0 ≤ c₀) (hc₁ : 0 ≤ c₁) (hd₀ : 0 ≤ d₀) (hd₁ : 0 ≤ d₁)
    (h₀₀ : a₀ * b₀ ≤ c₀ * d₀) (h₁₀ : a₁ * b₀ ≤ c₀ * d₁)
    (h₀₁ : a₀ * b₁ ≤ c₀ * d₁) (h₁₁ : a₁ * b₁ ≤ c₁ * d₁) :
    (a₀ + a₁) * (b₀ + b₁) ≤ (c₀ + c₁) * (d₀ + d₁)

Proof state:
β : Type u_2
inst✝¹ : LinearOrderedCommSemiring β
inst✝ : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : 0 < c₀ * d₁
⊢ a₀ * b₁ * (a₁ * b₀) + c₀ * d₁ * (c₀ * d₁) = a₀ * b₀ * (a₁ * b₁) + c₀ * d₁ * (c₀ * d₁)

Tactic:
ring

Result:
no goals

Proof state:
case inl
β : Type u_2
inst✝¹ : LinearOrderedCommSemiring β
inst✝ : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ 0
h₀₁ : a₀ * b₁ ≤ 0
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : c₀ * d₁ = 0
⊢ a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀

Tactic:
rw [h₀₁.antisymm, h₁₀.antisymm, add_zero] <;> positivity

Result:
no goals
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem quotientEquivQuotientMinpolyMap_symm_apply_mk (pb : PowerBasis R S) (I : Ideal R)
    (g : R[X]) :
    (pb.quotientEquivQuotientMinpolyMap I).symm (Ideal.Quotient.mk (Ideal.span
      ({(minpoly R pb.gen).map (Ideal.Quotient.mk I)} : Set (Polynomial (R ⧸ I))))
        (g.map (Ideal.Quotient.mk I))) = Ideal.Quotient.mk (I.map (algebraMap R S))
          (aeval pb.gen g)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pb : PowerBasis R S
I : Ideal R
g : R[X]
⊢ (pb.quotientEquivQuotientMinpolyMap I).symm
      ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
        (Polynomial.map (Ideal.Quotient.mk I) g)) =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval pb.gen) g)

Tactic:
simp only [quotientEquivQuotientMinpolyMap, toRingEquiv_eq_coe, symm_trans_apply,
  quotEquivQuotMap_symm_apply_mk, ofRingEquiv_symm_apply, quotientEquiv_symm_mk,
  toRingEquiv_symm, RingEquiv.symm_symm, AdjoinRoot.equiv'_apply, coe_ringEquiv, liftHom_mk,
  symm_toRingEquiv]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSq.lean
theorem mulExpNegMulSq_eq_sqrt_mul_mulExpNegMulSq_one (hε : 0 < ε) (x : ℝ) :
    mulExpNegMulSq ε x = (sqrt ε)⁻¹ * mulExpNegMulSq 1 (sqrt ε * x)

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
h✝ : √ε * x * (√ε * x) = ε * x * x
h : √ε = 0
⊢ False

Tactic:
rw [← pow_eq_zero_iff (Ne.symm (Nat.zero_ne_add_one 1)), sq_sqrt hε.le] at h

Result:
ε : ℝ
hε : 0 < ε
x : ℝ
h✝ : √ε * x * (√ε * x) = ε * x * x
h : ε = 0
⊢ False

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ √ε ^ 2 * x ^ 2 = x ^ 2 * ε

Tactic:
rw [sq_sqrt hε.le, mul_comm]

Result:
no goals

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
h : √ε * x * (√ε * x) = ε * x * x
⊢ x * rexp (-(ε * x * x)) = (√ε)⁻¹ * (√ε * x * rexp (-(√ε * x * (√ε * x))))

Tactic:
rw [h, eq_inv_mul_iff_mul_eq₀ _]

Result:
ε : ℝ
hε : 0 < ε
x : ℝ
h : √ε * x * (√ε * x) = ε * x * x
⊢ √ε * (x * rexp (-(ε * x * x))) = √ε * x * rexp (-(ε * x * x))

ε : ℝ
hε : 0 < ε
x : ℝ
h : √ε * x * (√ε * x) = ε * x * x
⊢ √ε ≠ 0

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ x * rexp (-(ε * x * x)) = (√ε)⁻¹ * (√ε * x * rexp (-(√ε * x * (√ε * x))))

Tactic:
have h : sqrt ε * x * (sqrt ε * x) = ε * x * x := by
  ring_nf
  rw [sq_sqrt hε.le, mul_comm]

Result:
ε : ℝ
hε : 0 < ε
x : ℝ
h : √ε * x * (√ε * x) = ε * x * x
⊢ x * rexp (-(ε * x * x)) = (√ε)⁻¹ * (√ε * x * rexp (-(√ε * x * (√ε * x))))

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ ε.mulExpNegMulSq x = (√ε)⁻¹ * mulExpNegMulSq 1 (√ε * x)

Tactic:
simp only [mulExpNegMulSq, one_mul]

Result:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ x * rexp (-(ε * x * x)) = (√ε)⁻¹ * (√ε * x * rexp (-(√ε * x * (√ε * x))))

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
h : √ε * x * (√ε * x) = ε * x * x
⊢ √ε * (x * rexp (-(ε * x * x))) = √ε * x * rexp (-(ε * x * x))

Tactic:
ring_nf

Result:
no goals

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ √ε * x * (√ε * x) = ε * x * x

Tactic:
ring_nf

Result:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ √ε ^ 2 * x ^ 2 = x ^ 2 * ε

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
h : √ε * x * (√ε * x) = ε * x * x
⊢ √ε ≠ 0

Tactic:
intro h

Result:
ε : ℝ
hε : 0 < ε
x : ℝ
h✝ : √ε * x * (√ε * x) = ε * x * x
h : √ε = 0
⊢ False

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
h✝ : √ε * x * (√ε * x) = ε * x * x
h : ε = 0
⊢ False

Tactic:
linarith

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem foldrM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : α → β → m β) (l : Vector α n) (init : β) :
    (l.filter p).foldrM g init =
      l.foldrM (fun x y => if p x then g x y else pure y) init

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : α → β → m β
init : β
l : Array α
⊢ Array.foldrM g init (Array.filter p { toArray := l, size_toArray := ⋯ }.toArray) =
    foldrM (fun x y => if p x = true then g x y else pure y) init { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.foldrM_filter]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : α → β → m β
l : Vector α n
init : β
⊢ Array.foldrM g init (Array.filter p l.toArray) = foldrM (fun x y => if p x = true then g x y else pure y) init l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : α → β → m β
init : β
l : Array α
⊢ Array.foldrM g init (Array.filter p { toArray := l, size_toArray := ⋯ }.toArray) =
    foldrM (fun x y => if p x = true then g x y else pure y) init { toArray := l, size_toArray := ⋯ }
-- Mathlib/Data/Multiset/Replicate.lean
theorem count_replicate (a b : α) (n : ℕ) : count a (replicate n b) = if b = a then n else 0

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ count a (replicate n b) = if b = a then n else 0

Tactic:
convert List.count_replicate a b n

Result:
case h.e'_2
α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ count a (replicate n b) = List.count a (List.replicate n b)

case h.e'_3.h₁.a
α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ b = a ↔ (b == a) = true

Proof state:
case h.e'_2
α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ count a (replicate n b) = List.count a (List.replicate n b)

Tactic:
rw [← coe_count, coe_replicate]

Result:
no goals

Proof state:
case h.e'_3.h₁.a
α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ b = a ↔ (b == a) = true

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem MemLp.eLpNorm_indicator_le' (hp_one : 1 ≤ p) (hp_top : p ≠ ∞) (hf : MemLp f p μ)
    (hmeas : StronglyMeasurable f) {ε : ℝ} (hε : 0 < ε) :
    ∃ (δ : ℝ) (_ : 0 < δ), ∀ s, MeasurableSet s → μ s ≤ ENNReal.ofReal δ →
      eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal ε

Proof state:
case intro.intro.intro.intro.refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ?m.104230 s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p ?m.104230 ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p (μ.restrict s) + eLpNorm ({x | ‖f x‖ < M}.indicator f) p (μ.restrict s) ≤
    ENNReal.ofReal ε + ENNReal.ofReal ε

Tactic:
refine add_le_add (le_trans (eLpNorm_mono_measure _ Measure.restrict_le_self) hM) ?_

Result:
case intro.intro.intro.intro.refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ?m.104230 s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p ?m.104230 ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm ({x | ‖f x‖ < M}.indicator f) p (μ.restrict s) ≤ ENNReal.ofReal ε
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
lemma num_le_mul_inv (I : FractionalIdeal R₁⁰ K) : I.num ≤ I * I⁻¹

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
⊢ ↑I.num ≤ I * I⁻¹

Tactic:
by_cases hI : I = 0

Result:
case pos
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : I = 0
⊢ ↑I.num ≤ I * I⁻¹

case neg
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : ¬I = 0
⊢ ↑I.num ≤ I * I⁻¹

Proof state:
case neg
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : ¬I = 0
⊢ ↑I.num ≤ I * I⁻¹

Tactic:
rw [mul_comm, ← den_mul_self_eq_num']

Result:
case neg
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : ¬I = 0
⊢ spanSingleton R₁⁰ ((algebraMap R₁ K) ↑I.den) * I ≤ I⁻¹ * I

Proof state:
case neg
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : ¬I = 0
⊢ spanSingleton R₁⁰ ((algebraMap R₁ K) ↑I.den) * I ≤ I⁻¹ * I

Tactic:
exact mul_right_mono I <| spanSingleton_le_iff_mem.2 (den_mem_inv hI)

Result:
no goals

Proof state:
case pos
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
hI : I = 0
⊢ ↑I.num ≤ I * I⁻¹

Tactic:
rw [hI, num_zero_eq <| FaithfulSMul.algebraMap_injective R₁ K, zero_mul, zero_eq_bot,
  coeIdeal_bot]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem smul_add_aux (x : T) (p q : LocalizedModule S M) :
    x • (p + q) = x • p + x • q

Proof state:
case h.h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
m : M
s : ↥S
n : M
t : ↥S
⊢ x • (mk m s + mk n t) = x • mk m s + x • mk n t

Tactic:
rw [smul_def, smul_def, mk_add_mk, mk_add_mk]

Result:
case h.h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
m : M
s : ↥S
n : M
t : ↥S
⊢ x • mk (t • m + s • n) (s * t) =
    mk
      (((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n)
      ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t))

Proof state:
case h.h.e_m
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
m : M
s : ↥S
n : M
t : ↥S
⊢ ((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S x).2 * ↑t) • m +
      ((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S x).2 * ↑s) • n =
    (↑(IsLocalization.sec S x).2 * ↑t * (IsLocalization.sec S x).1) • m +
      (↑(IsLocalization.sec S x).2 * ↑s * (IsLocalization.sec S x).1) • n

Tactic:
ring_nf

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem eq_iff_exists (f : LocalizationMap S N) {x y} :
    f.toMap x = f.toMap y ↔ ∃ c : S, ↑c * x = c * y := Iff.intro (f.4 x y)
  fun ⟨c, h⟩ ↦ by
    replace h := congr_arg f.toMap h
    rw [map_mul, map_mul] at h
    exact (f.map_units c).mul_right_inj.mp h

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
x✝ : ∃ c, ↑c * x = ↑c * y
c : ↥S
h : f.toMap (↑c * x) = f.toMap (↑c * y)
⊢ f.toMap x = f.toMap y

Tactic:
rw [map_mul, map_mul] at h

Result:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
x✝ : ∃ c, ↑c * x = ↑c * y
c : ↥S
h : f.toMap ↑c * f.toMap x = f.toMap ↑c * f.toMap y
⊢ f.toMap x = f.toMap y

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
x✝ : ∃ c, ↑c * x = ↑c * y
c : ↥S
h : ↑c * x = ↑c * y
⊢ f.toMap x = f.toMap y

Tactic:
replace h := congr_arg f.toMap h

Result:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
x✝ : ∃ c, ↑c * x = ↑c * y
c : ↥S
h : f.toMap (↑c * x) = f.toMap (↑c * y)
⊢ f.toMap x = f.toMap y

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
x✝ : ∃ c, ↑c * x = ↑c * y
c : ↥S
h : f.toMap ↑c * f.toMap x = f.toMap ↑c * f.toMap y
⊢ f.toMap x = f.toMap y

Tactic:
exact (f.map_units c).mul_right_inj.mp h

Result:
no goals
-- Mathlib/Topology/UniformSpace/Pi.lean
theorem uniformContinuous_pi {β : Type*} [UniformSpace β] {f : β → ∀ i, α i} :
    UniformContinuous f ↔ ∀ i, UniformContinuous fun x => f x i

Proof state:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
β : Type u_4
inst✝ : UniformSpace β
f : β → (i : ι) → α i
⊢ UniformContinuous f ↔ ∀ (i : ι), UniformContinuous fun x => f x i

Tactic:
simp only [UniformContinuous, Pi.uniformity, tendsto_iInf, tendsto_comap_iff, Function.comp_def]

Result:
no goals
-- Mathlib/Data/Set/Opposite.lean
theorem singleton_unop_op (x : αᵒᵖ) : ({unop x} : Set α).op = {x}

Proof state:
α : Type u_1
x : αᵒᵖ
⊢ {unop x}.op = {x}

Tactic:
ext

Result:
case h
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ {unop x}.op ↔ x✝ ∈ {x}

Proof state:
case h.mpr
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ {x} → x✝ ∈ {unop x}.op

Tactic:
apply op_injective

Result:
no goals

Proof state:
case h.mp
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ {unop x}.op → x✝ ∈ {x}

Tactic:
apply unop_injective

Result:
no goals

Proof state:
case h
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ {unop x}.op ↔ x✝ ∈ {x}

Tactic:
constructor

Result:
case h.mp
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ {unop x}.op → x✝ ∈ {x}

case h.mpr
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ {x} → x✝ ∈ {unop x}.op
-- Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
protected lemma add_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a + b :=
  numDenCasesOn' a fun n₁ d₁ h₁ ↦ numDenCasesOn' b fun n₂ d₂ h₂ ↦ by
    have d₁0 : 0 < (d₁ : ℤ) := mod_cast Nat.pos_of_ne_zero h₁
    have d₂0 : 0 < (d₂ : ℤ) := mod_cast Nat.pos_of_ne_zero h₂
    simp only [d₁0, d₂0, h₁, h₂, Int.mul_pos, divInt_nonneg_iff_of_pos_right, divInt_add_divInt, Ne,
      Nat.cast_eq_zero, not_false_iff]
    intro n₁0 n₂0
    apply Int.add_nonneg <;> apply Int.mul_nonneg <;> · first | assumption | apply Int.ofNat_zero_le

Proof state:
a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
⊢ 0 ≤ n₁ /. ↑d₁ → 0 ≤ n₂ /. ↑d₂ → 0 ≤ n₁ /. ↑d₁ + n₂ /. ↑d₂

Tactic:
have d₁0 : 0 < (d₁ : ℤ) := mod_cast Nat.pos_of_ne_zero h₁

Result:
a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
⊢ 0 ≤ n₁ /. ↑d₁ → 0 ≤ n₂ /. ↑d₂ → 0 ≤ n₁ /. ↑d₁ + n₂ /. ↑d₂

Proof state:
a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
⊢ 0 ≤ n₁ → 0 ≤ n₂ → 0 ≤ n₁ * ↑d₂ + n₂ * ↑d₁

Tactic:
intro n₁0 n₂0

Result:
a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
n₁0 : 0 ≤ n₁
n₂0 : 0 ≤ n₂
⊢ 0 ≤ n₁ * ↑d₂ + n₂ * ↑d₁

Proof state:
a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
⊢ 0 ≤ n₁ /. ↑d₁ → 0 ≤ n₂ /. ↑d₂ → 0 ≤ n₁ /. ↑d₁ + n₂ /. ↑d₂

Tactic:
have d₂0 : 0 < (d₂ : ℤ) := mod_cast Nat.pos_of_ne_zero h₂

Result:
a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
⊢ 0 ≤ n₁ /. ↑d₁ → 0 ≤ n₂ /. ↑d₂ → 0 ≤ n₁ /. ↑d₁ + n₂ /. ↑d₂

Proof state:
a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
⊢ 0 ≤ n₁ /. ↑d₁ → 0 ≤ n₂ /. ↑d₂ → 0 ≤ n₁ /. ↑d₁ + n₂ /. ↑d₂

Tactic:
simp only [d₁0, d₂0, h₁, h₂, Int.mul_pos, divInt_nonneg_iff_of_pos_right, divInt_add_divInt, Ne,
  Nat.cast_eq_zero, not_false_iff]

Result:
a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
⊢ 0 ≤ n₁ → 0 ≤ n₂ → 0 ≤ n₁ * ↑d₂ + n₂ * ↑d₁

Proof state:
case hb.hb
a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
n₁0 : 0 ≤ n₁
n₂0 : 0 ≤ n₂
⊢ 0 ≤ ↑d₁

Tactic:
apply Int.ofNat_zero_le

Result:
no goals

Proof state:
case hb.ha
a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
n₁0 : 0 ≤ n₁
n₂0 : 0 ≤ n₂
⊢ 0 ≤ n₂

Tactic:
assumption

Result:
no goals

Proof state:
case hb.hb
a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
n₁0 : 0 ≤ n₁
n₂0 : 0 ≤ n₂
⊢ 0 ≤ ↑d₁

Tactic:
first | assumption | apply Int.ofNat_zero_le

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem length_transfer (hp) : (p.transfer H hp).length = p.length

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ (p.transfer H hp).length = p.length

Tactic:
induction p <;> simp [*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem last_add_one : ∀ n, last n + 1 = 0
  | 0 => rfl
  | n + 1 => by ext; rw [val_add, val_zero, val_last, val_one, Nat.mod_self]

Proof state:
n : Nat
⊢ last (n + 1) + 1 = 0

Tactic:
ext

Result:
case h
n : Nat
⊢ ↑(last (n + 1) + 1) = ↑0

Proof state:
case h
n : Nat
⊢ ↑(last (n + 1) + 1) = ↑0

Tactic:
rw [val_add, val_zero, val_last, val_one, Nat.mod_self]

Result:
no goals
-- Mathlib/Data/PNat/Interval.lean
theorem card_fintype_Ioc : Fintype.card (Set.Ioc a b) = b - a

Proof state:
a b : ℕ+
⊢ Fintype.card ↑(Set.Ioc a b) = ↑b - ↑a

Tactic:
rw [← card_Ioc, Fintype.card_ofFinset]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma le_sub_iff_add_le {a b c : EReal} (hb : b ≠ ⊥ ∨ c ≠ ⊥) (ht : b ≠ ⊤ ∨ c ≠ ⊤) :
    a ≤ c - b ↔ a + b ≤ c

Proof state:
case h_top
a c : EReal
hb : ⊤ ≠ ⊥ ∨ c ≠ ⊥
ht : ¬c = ⊤
h : a + ⊤ ≤ c
⊢ a = ⊥

Tactic:
by_contra ha

Result:
case h_top
a c : EReal
hb : ⊤ ≠ ⊥ ∨ c ≠ ⊥
ht : ¬c = ⊤
h : a + ⊤ ≤ c
ha : ¬a = ⊥
⊢ False

Proof state:
case h_top
a c : EReal
hb : ⊤ ≠ ⊥ ∨ c ≠ ⊥
ht : ¬c = ⊤
⊢ a = ⊥ ↔ a + ⊤ ≤ c

Tactic:
refine ⟨fun h ↦ h ▸ (bot_add ⊤).symm ▸ bot_le, fun h ↦ ?_⟩

Result:
case h_top
a c : EReal
hb : ⊤ ≠ ⊥ ∨ c ≠ ⊥
ht : ¬c = ⊤
h : a + ⊤ ≤ c
⊢ a = ⊥

Proof state:
a b c : EReal
hb : b ≠ ⊥ ∨ c ≠ ⊥
ht : b ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c - b ↔ a + b ≤ c

Tactic:
induction b with
| h_bot =>
  simp only [ne_eq, not_true_eq_false, false_or] at hb
  simp only [sub_bot hb, le_top, add_bot, bot_le]
| h_real b =>
  rw [← (addLECancellable_coe b).add_le_add_iff_right, sub_add_cancel]
| h_top =>
  simp only [ne_eq, not_true_eq_false, false_or, sub_top, le_bot_iff] at ht ⊢
  refine ⟨fun h ↦ h ▸ (bot_add ⊤).symm ▸ bot_le, fun h ↦ ?_⟩
  by_contra ha
  exact (h.trans_lt (Ne.lt_top ht)).ne (add_top_iff_ne_bot.2 ha)

Result:
no goals

Proof state:
case h_top
a c : EReal
hb : ⊤ ≠ ⊥ ∨ c ≠ ⊥
ht : ⊤ ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c - ⊤ ↔ a + ⊤ ≤ c

Tactic:
simp only [ne_eq, not_true_eq_false, false_or, sub_top, le_bot_iff] at ht ⊢

Result:
case h_top
a c : EReal
hb : ⊤ ≠ ⊥ ∨ c ≠ ⊥
ht : ¬c = ⊤
⊢ a = ⊥ ↔ a + ⊤ ≤ c

Proof state:
case h_bot
a c : EReal
hb : ⊥ ≠ ⊥ ∨ c ≠ ⊥
ht : ⊥ ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c - ⊥ ↔ a + ⊥ ≤ c

Tactic:
simp only [ne_eq, not_true_eq_false, false_or] at hb

Result:
case h_bot
a c : EReal
ht : ⊥ ≠ ⊤ ∨ c ≠ ⊤
hb : ¬c = ⊥
⊢ a ≤ c - ⊥ ↔ a + ⊥ ≤ c

Proof state:
case h_real
a c : EReal
b : ℝ
hb : ↑b ≠ ⊥ ∨ c ≠ ⊥
ht : ↑b ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c - ↑b ↔ a + ↑b ≤ c

Tactic:
rw [← (addLECancellable_coe b).add_le_add_iff_right, sub_add_cancel]

Result:
no goals

Proof state:
case h_top
a c : EReal
hb : ⊤ ≠ ⊥ ∨ c ≠ ⊥
ht : ¬c = ⊤
h : a + ⊤ ≤ c
ha : ¬a = ⊥
⊢ False

Tactic:
exact (h.trans_lt (Ne.lt_top ht)).ne (add_top_iff_ne_bot.2 ha)

Result:
no goals

Proof state:
case h_bot
a c : EReal
ht : ⊥ ≠ ⊤ ∨ c ≠ ⊤
hb : ¬c = ⊥
⊢ a ≤ c - ⊥ ↔ a + ⊥ ≤ c

Tactic:
simp only [sub_bot hb, le_top, add_bot, bot_le]

Result:
no goals