mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Algebra

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 β)
hf : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (f y) 0
hg : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (g y) 0
H : ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 (α × β))
x : X
hx : x ∈ s
C : ℝ
hC : ∀ᶠ (a : X) in 𝓝[s] x, dist (f a) 0 ≤ C ∧ dist (g a) 0 ≤ C
n : ι
y : X
hFn : dist (f y) (F n y) < 1
hGn : dist (g y) (G n y) < 1
hfg : dist (f y) 0 ≤ C ∧ dist (g y) 0 ≤ C
⊢ dist (f y) 0 < C + 1 ∧ dist (g y) 0 < C + 1

Tactic:
constructor

Goal state after:
case left.left
α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 β)
hf : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (f y) 0
hg : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (g y) 0
H : ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 (α × β))
x : X
hx : x ∈ s
C : ℝ
hC : ∀ᶠ (a : X) in 𝓝[s] x, dist (f a) 0 ≤ C ∧ dist (g a) 0 ≤ C
n : ι
y : X
hFn : dist (f y) (F n y) < 1
hGn : dist (g y) (G n y) < 1
hfg : dist (f y) 0 ≤ C ∧ dist (g y) 0 ≤ C
⊢ dist (f y) 0 < C + 1

case left.right
α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 β)
hf : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (f y) 0
hg : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (g y) 0
H : ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 (α × β))
x : X
hx : x ∈ s
C : ℝ
hC : ∀ᶠ (a : X) in 𝓝[s] x, dist (f a) 0 ≤ C ∧ dist (g a) 0 ≤ C
n : ι
y : X
hFn : dist (f y) (F n y) < 1
hGn : dist (g y) (G n y) < 1
hfg : dist (f y) 0 ≤ C ∧ dist (g y) 0 ≤ C
⊢ dist (g y) 0 < C + 1
Module: Mathlib.Topology.MetricSpace.Algebra

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 β)
hf : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (f y) 0
hg : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (g y) 0
H : ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 (α × β))
x : X
hx : x ∈ s
C : ℝ
hC : ∀ᶠ (a : X) in 𝓝[s] x, dist (f a) 0 ≤ C ∧ dist (g a) 0 ≤ C
n : ι
y : X
hFn : dist (f y) (F n y) < 1
hGn : dist (g y) (G n y) < 1
hfg : dist (f y) 0 ≤ C ∧ dist (g y) 0 ≤ C
⊢ dist (f y) (F n y) + dist (f y) 0 < C + 1 ∧ dist (g y) (G n y) + dist (g y) 0 < C + 1

Tactic:
constructor

Goal state after:
case right.left
α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 β)
hf : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (f y) 0
hg : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (g y) 0
H : ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 (α × β))
x : X
hx : x ∈ s
C : ℝ
hC : ∀ᶠ (a : X) in 𝓝[s] x, dist (f a) 0 ≤ C ∧ dist (g a) 0 ≤ C
n : ι
y : X
hFn : dist (f y) (F n y) < 1
hGn : dist (g y) (G n y) < 1
hfg : dist (f y) 0 ≤ C ∧ dist (g y) 0 ≤ C
⊢ dist (f y) (F n y) + dist (f y) 0 < C + 1

case right.right
α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 β)
hf : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (f y) 0
hg : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (g y) 0
H : ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 (α × β))
x : X
hx : x ∈ s
C : ℝ
hC : ∀ᶠ (a : X) in 𝓝[s] x, dist (f a) 0 ≤ C ∧ dist (g a) 0 ≤ C
n : ι
y : X
hFn : dist (f y) (F n y) < 1
hGn : dist (g y) (G n y) < 1
hfg : dist (f y) 0 ≤ C ∧ dist (g y) 0 ≤ C
⊢ dist (g y) (G n y) + dist (g y) 0 < C + 1
Module: Mathlib.Topology.MetricSpace.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : TendstoLocallyUniformly F f l
hG : TendstoLocallyUniformly G g l
hf : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (f y) 0
hg : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (g y) 0
⊢ TendstoLocallyUniformly (F • G) (f • g) l

Tactic:
by
  rw [← tendstoLocallyUniformlyOn_univ] at *
  apply hF.smul₀_of_isBoundedUnder hG <;> simpa

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

Goal state before:
pp: case refine_1
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
x✝ : ∃ K, AntilipschitzWith K ⇑f
K : ℝ≥0
hK : AntilipschitzWith K ⇑f
x : E
⊢ (↑K + 1)⁻¹ * ‖x‖ ≤ ‖f x‖

Tactic:
grw [hK.le_mul_norm' (map_one f), ← mul_assoc]

Goal state after:
case refine_1
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
x✝ : ∃ K, AntilipschitzWith K ⇑f
K : ℝ≥0
hK : AntilipschitzWith K ⇑f
x : E
⊢ (↑K + 1)⁻¹ * ↑K * ‖f x‖ ≤ ‖f x‖
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: 𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
⊢ ‖x‖ = 1 ↔ x ≠ 0

Tactic:
constructor

Goal state after:
case mp
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
⊢ ‖x‖ = 1 → x ≠ 0

case mpr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
⊢ x ≠ 0 → ‖x‖ = 1
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: 𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
⊢ Metric.closedBall 0 1 = Set.univ

Tactic:
ext

Goal state after:
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x✝ : 𝕜
⊢ x✝ ∈ Metric.closedBall 0 1 ↔ x✝ ∈ Set.univ
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
⊢ x.toNNReal * ‖y‖₊ = ‖x * y‖₊

Tactic:
ext

Goal state after:
x y : ℝ
hx : 0 ≤ x
⊢ ↑(x.toNNReal * ‖y‖₊) = ↑‖x * y‖₊
Module: Mathlib.Topology.MetricSpace.DilationEquiv

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
e : X ≃ᵈ Y
⊢ ratio (refl Y) = 1

Tactic:
ratio_refl

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
e : X ≃ᵈ Y
⊢ 1 = 1
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: x : ℝ≥0
⊢ ‖↑x‖₊ = x

Tactic:
ext

Goal state after:
x : ℝ≥0
⊢ ↑‖↑x‖₊ = ↑x
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ (∃ x_1, dist x_1 x < ε ∧ s • x_1 = p) ↔ dist p (s • x) < ‖s‖ * ε

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ (∃ x_1, dist x_1 x < ε ∧ s • x_1 = p) → dist p (s • x) < ‖s‖ * ε

case mpr
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ dist p (s • x) < ‖s‖ * ε → ∃ x_1, dist x_1 x < ε ∧ s • x_1 = p
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ (∃ x_1, dist x_1 x ≤ ε ∧ s • x_1 = p) ↔ dist p (s • x) ≤ ‖s‖ * ε

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ (∃ x_1, dist x_1 x ≤ ε ∧ s • x_1 = p) → dist p (s • x) ≤ ‖s‖ * ε

case mpr
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ dist p (s • x) ≤ ‖s‖ * ε → ∃ x_1, dist x_1 x ≤ ε ∧ s • x_1 = p
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
m : ℕ
hm : -↑m < 0
⊢ Tendsto (fun x ↦ x ^ (-↑m)) (𝓝[≠] 0) (cobounded α)

Tactic:
simpa [Function.comp_def] using
    (tendsto_pow_cobounded_cobounded (by lia)).comp tendsto_inv₀_nhdsNE_zero

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

Goal state before:
pp: 𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
n : ℤ
x : 𝕜
⊢ ContinuousAt (fun x ↦ x ^ n) x ↔ x ≠ 0 ∨ 0 ≤ n

Tactic:
refine ⟨?_, continuousAt_zpow₀ _ _⟩

Goal state after:
𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
n : ℤ
x : 𝕜
⊢ ContinuousAt (fun x ↦ x ^ n) x → x ≠ 0 ∨ 0 ≤ n
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: K : Type u_4
inst✝ : NormedField K
⊢ CompleteSpace K ↔ IsComplete (closedBall 0 1)

Tactic:
constructor

Goal state after:
case mp
K : Type u_4
inst✝ : NormedField K
⊢ CompleteSpace K → IsComplete (closedBall 0 1)

case mpr
K : Type u_4
inst✝ : NormedField K
⊢ IsComplete (closedBall 0 1) → CompleteSpace K
Module: Mathlib.GroupTheory.GroupAction.IterateAct

Goal state before:
pp: α : Type u_1
f : α → α
a b c : IterateMulAct f
⊢ a * b * c = a * (b * c)

Tactic:
ext

Goal state after:
α : Type u_1
f : α → α
a b c : IterateMulAct f
⊢ (a * b * c).val = (a * (b * c)).val
Module: Mathlib.GroupTheory.GroupAction.IterateAct

Goal state before:
pp: α : Type u_1
f : α → α
x✝ : IterateMulAct f
⊢ 1 * x✝ = x✝

Tactic:
ext

Goal state after:
α : Type u_1
f : α → α
x✝ : IterateMulAct f
⊢ (1 * x✝).val = x✝.val
Module: Mathlib.GroupTheory.GroupAction.IterateAct

Goal state before:
pp: α : Type u_1
f : α → α
x✝ : IterateMulAct f
⊢ x✝ ^ 0 = 1

Tactic:
ext

Goal state after:
α : Type u_1
f : α → α
x✝ : IterateMulAct f
⊢ (x✝ ^ 0).val = val 1
Module: Mathlib.GroupTheory.GroupAction.IterateAct

Goal state before:
pp: α : Type u_1
f : α → α
n : ℕ
a : IterateMulAct f
⊢ a ^ (n + 1) = a ^ n * a

Tactic:
ext

Goal state after:
α : Type u_1
f : α → α
n : ℕ
a : IterateMulAct f
⊢ (a ^ (n + 1)).val = (a ^ n * a).val
Module: Mathlib.GroupTheory.GroupAction.IterateAct

Goal state before:
pp: α : Type u_1
f : α → α
x✝¹ x✝ : IterateMulAct f
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
ext

Goal state after:
α : Type u_1
f : α → α
x✝¹ x✝ : IterateMulAct f
⊢ (x✝¹ * x✝).val = (x✝ * x✝¹).val
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
⊢ Measurable (s.indicator fun x ↦ b) ↔ MeasurableSet s

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
⊢ Measurable (s.indicator fun x ↦ b) → MeasurableSet s

case mpr
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
⊢ MeasurableSet s → Measurable (s.indicator fun x ↦ b)
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet {x | p x}
ht : MeasurableSet {x | q x}
⊢ {x | p x ↔ q x} = {x | p x → q x} ∩ {x | q x → p x}

Tactic:
ext

Goal state after:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet {x | p x}
ht : MeasurableSet {x | q x}
x✝ : α
⊢ x✝ ∈ {x | p x ↔ q x} ↔ x✝ ∈ {x | p x → q x} ∩ {x | q x → p x}
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: case basic
α : Type u_1
C : Set (Set α)
p : (s : Set α) → MeasurableSet s → Prop
hC : ∀ t ∈ C, ∀ (ht : MeasurableSet t), p t ht
empty : p ∅ ⋯
compl : ∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯
iUnion : ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ i, s i) ⋯
s u✝ : Set α
a✝ : u✝ ∈ C
⊢ p u✝ ⋯

pp: case empty
α : Type u_1
C : Set (Set α)
p : (s : Set α) → MeasurableSet s → Prop
hC : ∀ t ∈ C, ∀ (ht : MeasurableSet t), p t ht
empty : p ∅ ⋯
compl : ∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯
iUnion : ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ i, s i) ⋯
s : Set α
⊢ p ∅ ⋯

pp: case compl
α : Type u_1
C : Set (Set α)
p : (s : Set α) → MeasurableSet s → Prop
hC : ∀ t ∈ C, ∀ (ht : MeasurableSet t), p t ht
empty : p ∅ ⋯
compl : ∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯
iUnion : ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ i, s i) ⋯
s t✝ : Set α
a✝ : GenerateMeasurable C t✝
a_ih✝ : p t✝ a✝
⊢ p t✝ᶜ ⋯

pp: case iUnion
α : Type u_1
C : Set (Set α)
p : (s : Set α) → MeasurableSet s → Prop
hC : ∀ t ∈ C, ∀ (ht : MeasurableSet t), p t ht
empty : p ∅ ⋯
compl : ∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯
iUnion : ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ i, s i) ⋯
s : Set α
f✝ : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable C (f✝ n)
a_ih✝ : ∀ (n : ℕ), p (f✝ n) ⋯
⊢ p (⋃ i, f✝ i) ⋯

Tactic:
exacts [hC _ ‹_› _, empty, compl _ ‹_› ‹_›, iUnion ‹_› ‹_› ‹_›]

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedField 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
E : Type u_6
inst✝² : SeminormedAddCommGroup E
h : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
⊢ restrictScalars 𝕜 𝕜' E = h

Tactic:
ext

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedField 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
E : Type u_6
inst✝² : SeminormedAddCommGroup E
h : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
x✝¹ : 𝕜
x✝ : E
⊢ SMul.smul x✝¹ x✝ = SMul.smul x✝¹ x✝
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedField 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
E : Type u_6
inst✝² : SeminormedAddCommGroup E
h : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
⊢ restrictScalars 𝕜 𝕜' E = h

Tactic:
ext
  apply algebraMap_smul

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ f ⁻¹' {false} = f ⁻¹' {true}ᶜ

Tactic:
Bool.compl_singleton,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ f ⁻¹' {false} = f ⁻¹' {!true}
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Norm E
inst✝ : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x : E
this : 0 = 0 • 0
⊢ ‖0‖ = 0

Tactic:
rw [this, core.norm_smul]

Goal state after:
𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Norm E
inst✝ : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x : E
this : 0 = 0 • 0
⊢ ‖0‖ * ‖0‖ = 0
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Norm E
inst✝ : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y : E
this : -y + x = -1 • (-x + y)
⊢ ‖-x + y‖ = ‖-y + x‖

Tactic:
rw [this, core.norm_smul]

Goal state after:
𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Norm E
inst✝ : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y : E
this : -y + x = -1 • (-x + y)
⊢ ‖-x + y‖ = ‖-1‖ * ‖-x + y‖
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
m : OuterMeasure α
⊢ LawfulFunctor OuterMeasure

Tactic:
constructor

Goal state after:
case map_const
α : Type u_1
β : Type u_2
m : OuterMeasure α
⊢ ∀ {α β : Type u_3}, Functor.mapConst = Functor.map ∘ const β

case id_map
α : Type u_1
β : Type u_2
m : OuterMeasure α
⊢ ∀ {α : Type u_3} (x : OuterMeasure α), id <$> x = x

case comp_map
α : Type u_1
β : Type u_2
m : OuterMeasure α
⊢ ∀ {α β γ : Type u_3} (g : α → β) (h : β → γ) (x : OuterMeasure α), (h ∘ g) <$> x = h <$> g <$> x
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
δ : Type u_4
X : δ → Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
⊢ MeasurableSpace.comap g (⨆ a, MeasurableSpace.comap (fun b ↦ b a) (inst✝ a)) ≤ inst✝¹ ↔
    ∀ (a : δ), MeasurableSpace.comap (fun x ↦ g x a) (inst✝ a) ≤ inst✝¹

Tactic:
MeasurableSpace.comap_iSup,

Goal state after:
α : Type u_1
δ : Type u_4
X : δ → Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
⊢ ⨆ i, MeasurableSpace.comap g (MeasurableSpace.comap (fun b ↦ b i) (inst✝ i)) ≤ inst✝¹ ↔
    ∀ (a : δ), MeasurableSpace.comap (fun x ↦ g x a) (inst✝ a) ≤ inst✝¹
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:
MeasurableSpace.comap_iSup,

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 a ↦ X a b) (MeasurableSpace.comap (fun b ↦ b i) (inst✝ i)) =
    ⨆ a, MeasurableSpace.comap (X a) inferInstance
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝¹ : MeasurableSpace β
g : β → Finset α
inst✝ : Countable α
S : Finset α
⊢ {s | ↑s ∈ {↑S}} = {S}

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝¹ : MeasurableSpace β
g : β → Finset α
inst✝ : Countable α
S x✝ : Finset α
⊢ x✝ ∈ {s | ↑s ∈ {↑S}} ↔ x✝ ∈ {S}
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableEq α
⊢ MeasurableSingletonClass α

Tactic:
constructor

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableEq α
⊢ ∀ (x : α), MeasurableSet {x}
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Countable α
⊢ MeasurableEq α

Tactic:
constructor

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Countable α
⊢ MeasurableSet (diagonal α)
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ zero ≤ zero

Tactic:
constructor

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ zero ≤ neg

Tactic:
constructor

Goal state after:
⊢ zero ≤ neg
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ zero ≤ pos

Tactic:
constructor

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ neg ≤ zero

Tactic:
constructor

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ neg ≤ neg

Tactic:
constructor

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ neg ≤ pos

Tactic:
constructor

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ pos ≤ zero

Tactic:
constructor

Goal state after:
⊢ pos ≤ zero
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ pos ≤ neg

Tactic:
constructor

Goal state after:
⊢ pos ≤ neg
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ pos ≤ pos

Tactic:
constructor

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero
⊢ zero ≤ zero

Tactic:
constructor

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case neg
⊢ neg ≤ neg

Tactic:
constructor

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos
⊢ pos ≤ pos

Tactic:
constructor

Goal state after:
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b, if g b = a then ↑(sgn b) else 0) = f a
⊢ Fintype.card (β ⊕ Fin (n - ∑ i ∈ s, (f i).natAbs)) = n

Tactic:
by simp [hβ, h]

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

Goal state before:
pp: R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousSMul R A
⊢ toSpanSingleton R 1 = algebraMapCLM R A

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousSMul R A
⊢ (toSpanSingleton R 1) 1 = (algebraMapCLM R A) 1
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : 0 < b
⊢ 1 ≤ 1

Tactic:
constructor

Goal state after: