mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝⁴ : Preorder α
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
x : ι
x_U : u x ≤ U
x_V : v x ≤ V
v_0 : 0 x ≤ v x
U_0 : 0 ≤ U
⊢ (u * v) x ≤ U * V

Tactic:
exact (mul_le_mul_of_nonneg_right x_U v_0).trans (mul_le_mul_of_nonneg_left x_V U_0)

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : Function.End α
K : ℝ≥0
h : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ (n + 1)) (f ^ (n + 1))

Tactic:
pow_succ,

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
f : Function.End α
K : ℝ≥0
h : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ n * K) (f ^ (n + 1))
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
K₁ K₂ : ℝ≥0
s : Set α
t : Set β
hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun x ↦ f x b) s
hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t
⊢ ∀ x ∈ s, ∀ y ∈ t, ∀ x_1 ∈ s, ∀ y_1 ∈ t, edist (f x y) (f x_1 y_1) ≤ ↑K₁ * Metric.ediam s + ↑K₂ * Metric.ediam t

Tactic:
intro a₁

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
K₁ K₂ : ℝ≥0
s : Set α
t : Set β
hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun x ↦ f x b) s
hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t
a₁ : α
⊢ a₁ ∈ s → ∀ y ∈ t, ∀ x ∈ s, ∀ y_1 ∈ t, edist (f a₁ y) (f x y_1) ≤ ↑K₁ * Metric.ediam s + ↑K₂ * Metric.ediam t
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : α → α
hf : LocallyLipschitz f
n : ℕ
⊢ LocallyLipschitz f^[n + 1]

Tactic:
rw [iterate_add, iterate_one]; exact (hf.iterate n).comp hf

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
h' : ∀ y > x, ∃ z, x < z ∧ z < y
⊢ limsup u f ≤ x

Tactic:
rw [← forall_gt_iff_le]

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
h' : ∀ y > x, ∃ z, x < z ∧ z < y
⊢ ∀ ⦃c : β⦄, x < c → limsup u f < c
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst✝ : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ (∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y) → limsup u f ≤ x

Tactic:
rw [← forall_gt_iff_le]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst✝ : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ (∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y) → ∀ ⦃c : β⦄, x < c → limsup u f < c
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.coe
a✝ : ℝ
h : ⊤ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ⊤ * ↑a✝ ≠ 0

Tactic:
rcases lt_or_gt_of_ne h.2 with (h | h)
        <;> simp [EReal.top_mul_of_pos, EReal.top_mul_of_neg, h]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
induction a, b using EReal.induction₂_symm with

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
by
  nth_rw 1 [← neg_zero]
  rw [EReal.le_neg, ← mul_neg, mul_nonneg_iff, EReal.neg_le, EReal.le_neg, neg_zero]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ a * b = ⊤ ↔ a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤

Tactic:
induction a, b using EReal.induction₂_symm with

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : Fintype β
f : β → α
L : SummationFilter β
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
h1 : ⋂ b ∈ L.support, {s | b ∈ s} ∈ L.filter
h2 : ⋂ b ∈ L.supportᶜ, {s | b ∉ s} ∈ L.filter
⊢ ∀ᶠ (x' : Finset β) in L.filter, ∏ b ∈ x', f b = ∏ b ∈ L.support.toFinset, f b

Tactic:
filter_upwards [h1, h2] with s hs hs'

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : Fintype β
f : β → α
L : SummationFilter β
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
h1 : ⋂ b ∈ L.support, {s | b ∈ s} ∈ L.filter
h2 : ⋂ b ∈ L.supportᶜ, {s | b ∉ s} ∈ L.filter
s : Finset β
hs : s ∈ ⋂ b ∈ L.support, {s | b ∈ s}
hs' : s ∈ ⋂ b ∈ L.supportᶜ, {s | b ∉ s}
⊢ ∏ b ∈ s, f b = ∏ b ∈ L.support.toFinset, f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
s : Finset β
f : β → α
L : SummationFilter ↑↑s
inst✝ : L.LeAtTop
⊢ HasProd (f ∘ Subtype.val) (∏ b ∈ s, f b) L

Tactic:
simpa [prod_attach, Embedding.subtype] using Finset.hasProd_support s f L

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
⊢ 1 ≤ ∏'[L] (i : ι), g i

Tactic:
by_cases hg : Multipliable g L

Goal state after:
case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : Multipliable g L
⊢ 1 ≤ ∏'[L] (i : ι), g i

case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : ¬Multipliable g L
⊢ 1 ≤ ∏'[L] (i : ι), g i
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 b)
hb : b ≠ ∞ ∨ a ≠ ∞
⊢ Tendsto (fun b ↦ a / m b) f (𝓝 (a / b))

Tactic:
apply Tendsto.const_mul (tendsto_inv_iff.2 hm)
  simp [hb]

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg✝ : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, f n ≤ b
a : ℝ≥0∞
hba : a > b
i : ι
hf : f i ≤ b
hg : g i ≤ a - b
⊢ (f + g) i ≤ a

Tactic:
calc f i + g i
    _ ≤ b + g i := by gcongr
    _ ≤ a := add_le_of_le_tsub_left_of_le hba.le hg

Goal state after:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case refine_2
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : ↑0 < ↑(1 / 2) ∧ ↑(1 / 2) < ↑1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), ↑(d x y) ≤ 2 * dist x y
n : ℕ
x✝ : True
x : X × X
hx : x ∉ U n
⊢ (1 / 2) ^ (n + 1) ≤ d x.1 x.2 / 2

Tactic:
pow_succ,

Goal state after:
case refine_2
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : ↑0 < ↑(1 / 2) ∧ ↑(1 / 2) < ↑1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), ↑(d x y) ≤ 2 * dist x y
n : ℕ
x✝ : True
x : X × X
hx : x ∉ U n
⊢ (1 / 2) ^ n * (1 / 2) ≤ d x.1 x.2 / 2
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x ↦ f ↑x + ↑K * dist y ↑x)
E : EqOn f g s
x y : α
z : ↑s
⊢ f ↑z + ↑K * dist x ↑z ≤ f ↑z + ↑K * dist y ↑z + ↑K * dist x y

Tactic:
rw [add_assoc, ← mul_add, add_comm (dist y z)]
      gcongr
      apply dist_triangle

Goal state after:
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: M : Type u
G : Type v
X : Type w
inst✝⁴ : PseudoEMetricSpace X
inst✝³ : SMul M X
inst✝² : SMul Mᵐᵒᵖ X
inst✝¹ : IsCentralScalar M X
inst✝ : IsIsometricSMul M X
c : Mᵐᵒᵖ
x y : X
⊢ edist ((fun x ↦ c • x) x) ((fun x ↦ c • x) y) = edist x y

Tactic:
simpa only [← op_smul_eq_smul] using! isometry_smul X c.unop x y

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → E
⊢ AntilipschitzWith K f⁻¹ ↔ AntilipschitzWith K f

Tactic:
by
  simp [AntilipschitzWith]

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)

Tactic:
by
  rw [dist_eq_norm, inv_sub_inv' hz hw, norm_mul, norm_mul, norm_inv, norm_inv, mul_comm ‖z‖⁻¹,
    mul_assoc, dist_eq_norm', div_eq_mul_inv, mul_inv]

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: case inl
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
𝕜 : Type u_5
h' : NormedField 𝕜
x : 𝕜
hx : x ≠ 0
hx1 : ‖x‖ ≠ 1
hlt : ‖x‖ < 1
⊢ ∃ x, 1 < ‖x‖

pp: case inr
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
𝕜 : Type u_5
h' : NormedField 𝕜
x : 𝕜
hx : x ≠ 0
hx1 : ‖x‖ ≠ 1
hlt : 1 < ‖x‖
⊢ ∃ x, 1 < ‖x‖

Tactic:
· use x⁻¹
      rw [norm_inv]
      exact (one_lt_inv₀ (norm_pos_iff.2 hx)).2 hlt

Goal state after:
case inr
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
𝕜 : Type u_5
h' : NormedField 𝕜
x : 𝕜
hx : x ≠ 0
hx1 : ‖x‖ ≠ 1
hlt : 1 < ‖x‖
⊢ ∃ x, 1 < ‖x‖
Module: Mathlib.Analysis.Normed.Group.Bounded

Goal state before:
pp: case inl
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf✝ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
hA : A ≤ 0
⊢ A * ‖f i‖ * ‖g i‖ < ε

Tactic:
exact (mul_nonpos_of_nonpos_of_nonneg (mul_nonpos_of_nonpos_of_nonneg hA <| norm_nonneg' _) <|
      norm_nonneg' _).trans_lt ε₀

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Bounded

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
⊢ ∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1

Tactic:
obtain ⟨K, ⟨hK1, hK2⟩⟩ := exists_compact_iff_hasCompactMulSupport.mpr hf
  obtain ⟨S, hS, hS'⟩ := hK1.isBounded.exists_pos_norm_le
  refine ⟨S + 1, by positivity, fun x hx => hK2 x ((mt <| hS' x) ?_)⟩
  contrapose! hx
  exact lt_add_of_le_of_pos hx zero_lt_one

Goal state after:
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: ι : Type u_1
π : ι → Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
hst : s ⊆ t
x : (i : ι) → π i
y : (i : ↥t) → π ↑i
i : ↥s
⊢ s.restrict (updateFinset x t y) i = restrict₂ hst y i

Tactic:
simp [updateFinset, dif_pos (hst i.2)]

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
⊢ comap Inv.inv (comap norm atTop) = 𝓝[≠] 0

Tactic:
← comap_norm_nhdsGT_zero,

Goal state after:
α : Type u_1
inst✝ : NormedDivisionRing α
⊢ comap Inv.inv (comap norm atTop) = comap norm (𝓝[>] 0)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
δ : Type u_4
X✝ : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X✝ a)
X : (a : δ) → β → X✝ a
⊢ MeasurableSpace.comap (fun b a ↦ X a b) inferInstance = ⨆ a, MeasurableSpace.comap (X a) inferInstance

Tactic:
simp_rw [MeasurableSpace.pi, MeasurableSpace.comap_iSup, MeasurableSpace.comap_comp]

Goal state after:
β : Type u_2
δ : Type u_4
X✝ : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X✝ a)
X : (a : δ) → β → X✝ a
⊢ ⨆ i, MeasurableSpace.comap ((fun b ↦ b i) ∘ fun b a ↦ X a b) (inst✝ i) =
    ⨆ a, MeasurableSpace.comap (X a) inferInstance
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : Nontrivial α
inst✝ : DecidableLT α
n : ℤ
⊢ sign ↑n = sign n

Tactic:
by
  simp only [sign_apply, Int.cast_pos, Int.cast_lt_zero]

Goal state after:
Module: Mathlib.Topology.Algebra.Algebra

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
toAlgHom✝¹ : A →ₐ[R] B
cont✝¹ : Continuous[inst✝⁴, inst✝²] (↑↑toAlgHom✝¹.toRingHom).toFun
toAlgHom✝ : A →ₐ[R] B
cont✝ : Continuous[inst✝⁴, inst✝²] (↑↑toAlgHom✝.toRingHom).toFun
h :
  (fun f ↦ ⇑f.toAlgHom) { toAlgHom := toAlgHom✝¹, cont := cont✝¹ } =
    (fun f ↦ ⇑f.toAlgHom) { toAlgHom := toAlgHom✝, cont := cont✝ }
⊢ { toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = { toAlgHom := toAlgHom✝, cont := cont✝ }

Tactic:
simp only [mk.injEq]

Goal state after:
case mk.mk
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
toAlgHom✝¹ : A →ₐ[R] B
cont✝¹ : Continuous[inst✝⁴, inst✝²] (↑↑toAlgHom✝¹.toRingHom).toFun
toAlgHom✝ : A →ₐ[R] B
cont✝ : Continuous[inst✝⁴, inst✝²] (↑↑toAlgHom✝.toRingHom).toFun
h :
  (fun f ↦ ⇑f.toAlgHom) { toAlgHom := toAlgHom✝¹, cont := cont✝¹ } =
    (fun f ↦ ⇑f.toAlgHom) { toAlgHom := toAlgHom✝, cont := cont✝ }
⊢ toAlgHom✝¹ = toAlgHom✝
Module: Mathlib.Topology.Algebra.Algebra

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
toAlgHom✝¹ : A →ₐ[R] B
cont✝¹ : Continuous[inst✝⁴, inst✝²] (↑↑toAlgHom✝¹.toRingHom).toFun
toAlgHom✝ : A →ₐ[R] B
cont✝ : Continuous[inst✝⁴, inst✝²] (↑↑toAlgHom✝.toRingHom).toFun
⊢ ↑{ toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = ↑{ toAlgHom := toAlgHom✝, cont := cont✝ } ↔
    { toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = { toAlgHom := toAlgHom✝, cont := cont✝ }

Tactic:
simp only [mk.injEq]

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b : EReal
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
induction a, b using EReal.induction₂_symm with

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
⊢ a / b / c = a / (b * c)

Tactic:
change (a * b⁻¹) * c⁻¹ = a * (b * c)⁻¹

Goal state after:
a b c : EReal
⊢ a * b⁻¹ * c⁻¹ = a * (b * c)⁻¹
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsOpen[inst✝²] s
hy : 0 ≤ y
⊢ LowerSemicontinuous (s.indicator fun _x ↦ y)

Tactic:
intro x z hz
  by_cases h : x ∈ s <;> simp [h] at hz
  · filter_upwards [hs.mem_nhds h]
    simp +contextual [hz]
  · refine Filter.Eventually.of_forall fun x' => ?_
    by_cases h' : x' ∈ s <;> simp [h', hz.trans_le hy, hz]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝ : CompleteLinearOrder γ
f : α → γ
⊢ LowerSemicontinuousWithinAt f s x → f x ≤ liminf f (𝓝[s] x)

pp: case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝ : CompleteLinearOrder γ
f : α → γ
⊢ f x ≤ liminf f (𝓝[s] x) → LowerSemicontinuousWithinAt f s x

Tactic:
· intro h; unfold LowerSemicontinuousWithinAt at h
    by_contra! hf
    obtain ⟨z, ltz, y, ylt, h₁⟩ := hf.exists_disjoint_Iio_Ioi
    exact ltz.not_ge
      (le_liminf_of_le (by isBoundedDefault) ((h y ylt).mono fun _ h₂ =>
        le_of_not_gt fun h₃ => (h₁ _ h₃ _ h₂).false))

Goal state after:
case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝ : CompleteLinearOrder γ
f : α → γ
⊢ f x ≤ liminf f (𝓝[s] x) → LowerSemicontinuousWithinAt f s x
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u_0 : 0 ≤ limsup u f
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
⊢ limsup (u * v) f ≤ limsup u f * limsup v f

Tactic:
refine le_mul_of_forall_lt h₁ h₂ fun a a_u b b_v ↦ (limsup_le_iff).2 fun c c_ab ↦ ?_

Goal state after:
case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u_0 : 0 ≤ limsup u f
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a * b
⊢ ∀ᶠ (a : α) in f, (u * v) a < c
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, u (k + 1) ≤ c * u k
⊢ u n ≤ c ^ n * u 0

Tactic:
apply (monotone_mul_left_of_nonneg hc).seq_le_seq n _ h _

Goal state after:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, u (k + 1) ≤ c * u k
⊢ u 0 ≤ c ^ 0 * u 0

u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, u (k + 1) ≤ c * u k
⊢ ∀ k < n, c * (c ^ k * u 0) ≤ c ^ (k + 1) * u 0
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0
hr : r < 1
⊢ Tendsto (fun a ↦ ↑(r ^ a)) atTop (𝓝 ↑0)

Tactic:
simp only [NNReal.coe_pow, NNReal.coe_zero,
      _root_.tendsto_pow_atTop_nhds_zero_of_lt_one r.coe_nonneg hr]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
hf : LowerSemicontinuousWithinAt f univ x
hg : LowerSemicontinuousWithinAt g univ x
⊢ LowerSemicontinuousWithinAt (fun z ↦ f z + g z) univ x

Tactic:
exact hf.add' hg hcont

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_2
α : Type u_1
m : Set (OuterMeasure α)
⊢ boundedBy (sInfGen m) ≤ sInf m

Tactic:
refine le_sInf ?_
    intro μ hμ t
    exact le_trans (boundedBy_le t) (iInf₂_le μ hμ)

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_4
inst✝³ : TopologicalSpace α
β : Type u_5
f : α → β
s : Set α
inst✝² : PartialOrder β
inst✝¹ : CommGroup β
inst✝ : IsOrderedMonoid β
⊢ UpperSemicontinuousOn f⁻¹ s ↔ LowerSemicontinuousOn f s

Tactic:
simp [← lowerSemicontinuousOn_inv_iff]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
hf : UpperSemicontinuousWithinAt f univ x
hg : UpperSemicontinuousWithinAt g univ x
⊢ UpperSemicontinuousWithinAt (fun z ↦ f z + g z) univ x

Tactic:
exact hf.add' hg hcont

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
h : s ∈ π i ∨ s ∈ {univ}
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}

Tactic:
rcases h with hs | hs

Goal state after:
case refine_2.inl
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}

case refine_2.inr
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ {univ}
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S) ≤ generateFrom {s | MeasurableSet s}

Tactic:
exact generateFrom_mono (measurableSet_iSup_of_mem_piiUnionInter m S)

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
⊢ ∀ (s : ℕ → Set α), extend m (⋃ i, s i) ≤ ∑' (i : ℕ), extend m (s i)

Tactic:
refine extend_iUnion_le_tsum_nat' MeasurableSet.iUnion ?_

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
⊢ ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : MeasurableSpace α
ι : Type u_5
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Monotone s
hs : ∀ (i : ι), MeasurableSet (s i)
h✝ : IsEmpty ι
⊢ MeasurableSet (⋃ i, s i)

Tactic:
| inl _ =>

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m₁ m₂ m₃ : OuterMeasure α
op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞
h : ∀ (s : Set α), m₁ s = op (m₂ s) (m₃ s)
s t : Set α
_hst : s ⊆ t
_ht : MeasurableSet t
htm : ∀ (i : Fin (Nat.succ 0).succ.succ), (![m₁, m₂, m₃] i) t = (![m₁, m₂, m₃] i).trim s
⊢ m₁.trim s = op (m₂.trim s) (m₃.trim s)

Tactic:
simp only [Fin.forall_iff_succ, Matrix.cons_val_zero, Matrix.cons_val_succ] at htm

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
m₁ m₂ m₃ : OuterMeasure α
op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞
h : ∀ (s : Set α), m₁ s = op (m₂ s) (m₃ s)
s t : Set α
_hst : s ⊆ t
_ht : MeasurableSet t
htm : m₁ t = m₁.trim s ∧ m₂ t = m₂.trim s ∧ m₃ t = m₃.trim s ∧ ∀ (i : Fin 0), (![] i) t = (![] i).trim s
⊢ m₁.trim s = op (m₂.trim s) (m₃.trim s)
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
m : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
μ : Measure α
g : β → γ
hg : Measurable g
hf : NullMeasurable f μ
⊢ NullMeasurable (g ∘ f) μ

Tactic:
rw [nullMeasurable_iff_eventuallyMeasurable]

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
m : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
μ : Measure α
g : β → γ
hg : Measurable g
hf : NullMeasurable f μ
⊢ EventuallyMeasurable m (ae μ) (g ∘ f)