mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
k0 : k = 0
⊢ R < ω ^ (a0.repr * succ ↑k)

Tactic:
simp only [k0, Nat.cast_zero, succ_eq_add_one, _root_.zero_add, mul_one, R]

Goal state after:
case pos
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
k0 : k = 0
⊢ (opowAux 0 a0 (a0.oadd n a' * ↑m) 0 m).repr < ω ^ a0.repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op op' : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
h' : FriendlyOperation op'
⊢ FriendlyOperation (op ∘ op')

Tactic:
FriendlyOperation

Goal state after:
α : Type u_1
op op' : Stream'.Seq α → Stream'.Seq α
h : LipschitzWith 1 op
h' : LipschitzWith 1 op'
⊢ LipschitzWith 1 (op ∘ op')
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op₁ op₂ : Stream'.Seq α → Stream'.Seq α
h₁ : FriendlyOperation op₁
h₂ : FriendlyOperation op₂
P : Option α → Prop
inst✝ : DecidablePred P
⊢ FriendlyOperation fun s ↦ if P s.head then op₁ s else op₂ s

Tactic:
friendlyOperation_iff_dist_le_dist

Goal state after:
α : Type u_1
op₁ op₂ : Stream'.Seq α → Stream'.Seq α
h₁ : ∀ (s t : Stream'.Seq α), dist (op₁ s) (op₁ t) ≤ dist s t
h₂ : ∀ (s t : Stream'.Seq α), dist (op₂ s) (op₂ t) ≤ dist s t
P : Option α → Prop
inst✝ : DecidablePred P
⊢ ∀ (s t : Stream'.Seq α), dist (if P s.head then op₁ s else op₂ s) (if P t.head then op₁ t else op₂ t) ≤ dist s t
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
h : FriendlyOperation op
⊢ FriendlyOperation fun s ↦ (op (Seq.cons hd s)).tail

Tactic:
friendlyOperation_iff_dist_le_dist

Goal state after:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
h : ∀ (s t : Stream'.Seq α), dist (op s) (op t) ≤ dist s t
⊢ ∀ (s t : Stream'.Seq α), dist (op (Seq.cons hd s)).tail (op (Seq.cons hd t)).tail ≤ dist s t
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
a : α
s t : Stream'.Seq α
⊢ (op (Seq.cons a s)).head = (op (Seq.cons a t)).head

Tactic:
friendlyOperation_iff_dist_le_dist

Goal state after:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : ∀ (s t : Stream'.Seq α), dist (op s) (op t) ≤ dist s t
a : α
s t : Stream'.Seq α
⊢ (op (Seq.cons a s)).head = (op (Seq.cons a t)).head
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : ∀ (s t : Stream'.Seq α) (n : ℕ), dist s t ≤ 2⁻¹ ^ n → dist (op s) (op t) ≤ 2⁻¹ ^ n
⊢ FriendlyOperation op

Tactic:
friendlyOperation_iff_dist_le_dist

Goal state after:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : ∀ (s t : Stream'.Seq α) (n : ℕ), dist s t ≤ 2⁻¹ ^ n → dist (op s) (op t) ≤ 2⁻¹ ^ n
⊢ ∀ (s t : Stream'.Seq α), dist (op s) (op t) ≤ dist s t
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case succ.none
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, op') => (hd, ↑op' s.tail))
              (T s.head)
n : ℕ
ih :
  ∀ {op : Stream'.Seq α → Stream'.Seq α},
    motive op → ∀ (s t : Stream'.Seq α), dist s t ≤ 2⁻¹ ^ n → dist (op s) (op t) ≤ 2⁻¹ ^ n
op : Stream'.Seq α → Stream'.Seq α
h_base : motive op
s t : Stream'.Seq α
hn : dist s t ≤ 2⁻¹ ^ (n + 1)
T : Option α → Option (α × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, op') => (hd, ↑op' s.tail))
        (T s.head)
h_head : s.head = t.head
hs :
  (op s).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' s.tail))
      (T s.head)
ht :
  (op t).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' t.tail))
      (T t.head)
hT_head : T s.head = none
⊢ dist (op s) (op t) ≤ 2⁻¹ ^ (n + 1)

Tactic:
simp only [hT_head, Option.map_none, ← h_head] at hs ht
      simp [hs, ht, destruct_eq_none]

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: m : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_length : List.length m = List.length basis_tl
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ Majorized (m.toFun basis_tl) basis_hd 0

Tactic:
induction m generalizing basis_hd basis_tl with
  | nil =>
    simp only [toFun_nil]
    exact Majorized.const (h_basis.tendsto_atTop (by simp))
  | cons hd tl ih =>
    cases basis_tl with
    | nil => simp at h_length
    | cons basis_tl_hd basis_tl_tl =>
      simp only [List.length_cons, Nat.add_right_cancel_iff, toFun_cons] at h_length ⊢
      rw [← add_zero 0]
      apply Majorized.mul (h_basis.tail_pow_majorized_head (by simp) _) _
        h_basis.head_eventually_pos
      exact fun exp h_exp ↦
        (ih h_length h_basis.tail 1 (by simp)).trans <|
        h_basis.tail_pow_majorized_head (by simp) 1 exp h_exp

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
⊢ t.inv.toFun basis =ᶠ[atTop] (t.toFun basis)⁻¹

Tactic:
by
  simp only [toFun, inv]
  grw [UnitMonomial.inv_toFun h_basis]
  filter_upwards [] with x
  simp [Pi.smul_apply, Pi.inv_apply]
  ring

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case h
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = op' ∘ opf ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
        (T s.head)
s s' : Stream'.Seq α
hF :
  s'.destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' s.tail))
      (h_opf.unfold s.head)
⊢ (op s').destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s.tail))
      (match h_opf.unfold s.head with
      | none => Option.map (fun x ↦ (x.1, ⟨↑x.2.2 ∘ fun x_1 ↦ ↑x.2.1 nil, ⋯⟩)) (T none)
      | some (hd, opf') => Option.map (fun x ↦ (x.1, ⟨↑x.2.2 ∘ ↑x.2.1 ∘ ↑opf', ⋯⟩)) (T (some hd)))

Tactic:
cases s' with
  | nil =>
    symm at hF
    simp only [destruct_nil, Option.map_eq_none_iff] at hF
    simp only [hF, Option.map_map]
    specialize hT nil
    simp only [tail_nil, head_nil] at hT
    simp [hT]
    rfl
  | cons s_hd s_tl =>
  simp only [destruct_cons] at hF
  generalize h_opf.unfold s.head = t? at *
  cases t? with
  | none => simp at hF
  | some v =>
  obtain ⟨hd, opf', op'⟩ := v
  simp only [Option.map_some, Option.some.injEq, Prod.mk.injEq] at hF
  simp only [hF, Option.map_map]
  rw [hT]
  rfl

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.IsZero
⊢ ms.seq = Multiseries.nil

Tactic:
cases h; rw [mk_seq]

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: s : S
⊢ S.decode s.encode = s

Tactic:
by
    induction s with
    | nat n =>
      unfold S.encode S.decode
      simp
    | cons a b iha ihb =>
      unfold S.encode S.decode
      simp [iha, ihb]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: x✝ : ONote
o : ONote := x✝
a : ONote
h : o.FundamentalSequenceProp (Sum.inl (some a))
⊢ a.repr < succ a.repr

Tactic:
apply lt_succ

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: i : ℕ
⊢ Nat.succ^[i] i = i + i

Tactic:
exact Nat.succ_iterate _ _

Goal state after:
Module: Mathlib.Tactic.ITauto

Goal state before:
pp: case var.true
a✝ : Nat
⊢ Ordering

pp: case var.false
a✝ : Nat
⊢ Ordering

pp: case var.and'
a✝³ : Nat
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case var.or
a✝² : Nat
a✝¹ a✝ : IProp
⊢ Ordering

pp: case var.imp
a✝² : Nat
a✝¹ a✝ : IProp
⊢ Ordering

pp: case true.var
a✝ : Nat
⊢ Ordering

pp: case true.false
⊢ Ordering

pp: case true.and'
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case true.or
a✝¹ a✝ : IProp
⊢ Ordering

pp: case true.imp
a✝¹ a✝ : IProp
⊢ Ordering

pp: case false.var
a✝ : Nat
⊢ Ordering

pp: case false.true
⊢ Ordering

pp: case false.and'
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case false.or
a✝¹ a✝ : IProp
⊢ Ordering

pp: case false.imp
a✝¹ a✝ : IProp
⊢ Ordering

pp: case and'.var
a✝³ : AndKind
a✝² a✝¹ : IProp
a✝ : Nat
⊢ Ordering

pp: case and'.true
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case and'.false
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case and'.or
a✝⁴ : AndKind
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

pp: case and'.imp
a✝⁴ : AndKind
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

pp: case or.var
a✝² a✝¹ : IProp
a✝ : Nat
⊢ Ordering

pp: case or.true
a✝¹ a✝ : IProp
⊢ Ordering

pp: case or.false
a✝¹ a✝ : IProp
⊢ Ordering

pp: case or.and'
a✝⁴ a✝³ : IProp
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case or.imp
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

pp: case imp.var
a✝² a✝¹ : IProp
a✝ : Nat
⊢ Ordering

pp: case imp.true
a✝¹ a✝ : IProp
⊢ Ordering

pp: case imp.false
a✝¹ a✝ : IProp
⊢ Ordering

pp: case imp.and'
a✝⁴ a✝³ : IProp
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case imp.or
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

pp: case imp.imp
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

Tactic:
case imp.imp p₁ p₂ q₁ q₂ => exact (p₁.cmp q₁).then (p₂.cmp q₂)

Goal state after:
case var.true
a✝ : Nat
⊢ Ordering

case var.false
a✝ : Nat
⊢ Ordering

case var.and'
a✝³ : Nat
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case var.or
a✝² : Nat
a✝¹ a✝ : IProp
⊢ Ordering

case var.imp
a✝² : Nat
a✝¹ a✝ : IProp
⊢ Ordering

case true.var
a✝ : Nat
⊢ Ordering

case true.false
⊢ Ordering

case true.and'
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case true.or
a✝¹ a✝ : IProp
⊢ Ordering

case true.imp
a✝¹ a✝ : IProp
⊢ Ordering

case false.var
a✝ : Nat
⊢ Ordering

case false.true
⊢ Ordering

case false.and'
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case false.or
a✝¹ a✝ : IProp
⊢ Ordering

case false.imp
a✝¹ a✝ : IProp
⊢ Ordering

case and'.var
a✝³ : AndKind
a✝² a✝¹ : IProp
a✝ : Nat
⊢ Ordering

case and'.true
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case and'.false
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case and'.or
a✝⁴ : AndKind
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

case and'.imp
a✝⁴ : AndKind
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

case or.var
a✝² a✝¹ : IProp
a✝ : Nat
⊢ Ordering

case or.true
a✝¹ a✝ : IProp
⊢ Ordering

case or.false
a✝¹ a✝ : IProp
⊢ Ordering

case or.and'
a✝⁴ a✝³ : IProp
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case or.imp
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

case imp.var
a✝² a✝¹ : IProp
a✝ : Nat
⊢ Ordering

case imp.true
a✝¹ a✝ : IProp
⊢ Ordering

case imp.false
a✝¹ a✝ : IProp
⊢ Ordering

case imp.and'
a✝⁴ a✝³ : IProp
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case imp.or
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering
Module: Mathlib.Tactic.NormNum.NatLog

Goal state before:
pp: b m n : ℕ
hb : Nat.blt 1 b = true
h₁ : (b ^ m).blt n = true
h₂ : n.ble (b ^ (m + 1)) = true
⊢ Nat.clog b n = m + 1

Tactic:
rw [Nat.blt_eq] at hb
  rw [Nat.blt_eq, ← Nat.lt_clog_iff_pow_lt hb] at h₁
  rw [Nat.ble_eq, ← Nat.clog_le_iff_le_pow hb] at h₂
  lia

Goal state after:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case neg
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : a * y ^ d = x ^ d * b
⊢ False

Tactic:
apply ha

Goal state after:
case neg
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := ⋯
y : ℕ := ⋯
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : a * y ^ d = x ^ d * b
⊢ a = x ^ d
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
hy_inv : Invertible ↑y_den
hy_eq : y = ↑y_num * ⅟↑y_den
h1 : ↑y_num * ⅟↑y_den = ↑(↑y_num / ↑y_den)
h2 : ↑x_num * ⅟↑x_den = ↑(↑x_num / ↑x_den)
⊢ Irrational ((↑x_num * ⅟↑x_den) ^ (↑y_num * ⅟↑y_den))

Tactic:
h1,

Goal state after:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
hy_inv : Invertible ↑y_den
hy_eq : y = ↑y_num * ⅟↑y_den
h1 : ↑y_num * ⅟↑y_den = ↑(↑y_num / ↑y_den)
h2 : ↑x_num * ⅟↑x_den = ↑(↑x_num / ↑x_den)
⊢ Irrational ((↑x_num * ⅟↑x_den) ^ ↑(↑y_num / ↑y_den))
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
E' : Type u_5
F' : Type u_6
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommMonoid F
inst✝² : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝¹ : ContinuousAdd 𝕜
inst✝ : ContinuousConstSMul 𝕜 𝕜
x✝¹ x✝ : F
⊢ { toLinearMap := B.flip (x✝¹ + x✝), cont := ⋯ } =
    { toLinearMap := B.flip x✝¹, cont := ⋯ } + { toLinearMap := B.flip x✝, cont := ⋯ }

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
E' : Type u_5
F' : Type u_6
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommMonoid F
inst✝² : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝¹ : ContinuousAdd 𝕜
inst✝ : ContinuousConstSMul 𝕜 𝕜
x✝¹ : 𝕜
x✝ : F
⊢ { toLinearMap := B.flip (x✝¹ • x✝), cont := ⋯ } = (RingHom.id 𝕜) x✝¹ • { toLinearMap := B.flip x✝, cont := ⋯ }

Tactic:
by ext; simp

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

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
f : E →ₛₗ[σ] F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : RingHomIsometric σ
V : Set E
V_mem : V ∈ 𝓝 0
H : IsInducing (V.domRestrict ⇑f)
this : IsTopologicalAddGroup E
⊢ inst✝⁶ = TopologicalSpace.induced (⇑f) inst✝⁵

Tactic:
have := continuousSMul_inducedₛₗ f σ.isometry.continuous

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
f : E →ₛₗ[σ] F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : RingHomIsometric σ
V : Set E
V_mem : V ∈ 𝓝 0
H : IsInducing (V.domRestrict ⇑f)
this✝ : IsTopologicalAddGroup E
this : ContinuousSMul 𝕜₁ E
⊢ inst✝⁶ = TopologicalSpace.induced (⇑f) inst✝⁵
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
f : E →ₛₗ[σ] F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : RingHomIsometric σ
V : Set E
V_mem : V ∈ 𝓝 0
H : IsEmbedding (V.domRestrict ⇑f)
f_injOn : InjOn (⇑f) V
⊢ Function.Injective ⇑f

Tactic:
rw [← LinearMap.ker_eq_bot, Submodule.eq_bot_iff]

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
f : E →ₛₗ[σ] F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : RingHomIsometric σ
V : Set E
V_mem : V ∈ 𝓝 0
H : IsEmbedding (V.domRestrict ⇑f)
f_injOn : InjOn (⇑f) V
⊢ ∀ x ∈ f.ker, x = 0
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : InvolutiveStar R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : Module R E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module R F
inst✝⁵ : StarAddMonoid F
inst✝⁴ : StarModule R F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousStar E
inst✝ : ContinuousStar F
x : WithConv (E →L[R] F)
⊢ star (star x) = x

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : InvolutiveStar R
inst✝¹² : AddCommMonoid E
inst✝¹¹ : Module R E
inst✝¹⁰ : StarAddMonoid E
inst✝⁹ : StarModule R E
inst✝⁸ : AddCommMonoid F
inst✝⁷ : Module R F
inst✝⁶ : StarAddMonoid F
inst✝⁵ : StarModule R F
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : ContinuousStar E
inst✝¹ : ContinuousStar F
inst✝ : ContinuousAdd F
x y : WithConv (E →L[R] F)
⊢ star (x + y) = star x + star y

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : InvolutiveStar R
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module R E
inst✝³ : StarAddMonoid E
inst✝² : StarModule R E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousStar E
⊢ star (toConv (ContinuousLinearMap.id R E)) = toConv (ContinuousLinearMap.id R E)

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : InvolutiveStar R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : Module R E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module R F
inst✝⁵ : StarAddMonoid F
inst✝⁴ : StarModule R F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousStar E
inst✝ : ContinuousStar F
⊢ star (toConv 0) = toConv 0

Tactic:
by ext; simp

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

Goal state before:
pp: E : Type u_2
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : StarAddMonoid E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : ContinuousStar E
S : Type u_4
inst✝⁷ : Semiring S
inst✝⁶ : StarAddMonoid S
inst✝⁵ : StarModule S S
inst✝⁴ : Module S E
inst✝³ : StarModule S E
inst✝² : TopologicalSpace S
inst✝¹ : ContinuousStar S
inst✝ : ContinuousSMul S E
a : E
⊢ star (toConv (toSpanSingleton S a)) = toConv (toSpanSingleton S (star a))

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁵ : Semiring R
inst✝¹⁴ : InvolutiveStar R
inst✝¹³ : AddCommMonoid E
inst✝¹² : Module R E
inst✝¹¹ : StarAddMonoid E
inst✝¹⁰ : StarModule R E
inst✝⁹ : AddCommMonoid F
inst✝⁸ : Module R F
inst✝⁷ : StarAddMonoid F
inst✝⁶ : StarModule R F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : ContinuousStar E
inst✝² : ContinuousStar F
inst✝¹ : SMulCommClass R R F
inst✝ : ContinuousConstSMul R F
x✝¹ : R
x✝ : WithConv (E →L[R] F)
⊢ star (x✝¹ • x✝) = star x✝¹ • star x✝

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
this : ∀ S ∈ T2, S ∈ T0 ∨ ∃ Q ∈ T0, S = AA ∩ Q
⊢ ∀ S ∈ T2, S.Nonempty

Tactic:
intro S hS
      rcases this _ hS with h | h
      · exact claim5 S h
      · rcases h with ⟨Q, hQ, rfl⟩
        exact claim4 Q hQ

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : ↑C
i : ι
h : (π_app C fun x ↦ x ∈ {i}) a = (π_app C fun x ↦ x ∈ {i}) b
⊢ ↑a i = ↑b i

Tactic:
rw [Subtype.ext_iff] at h

Goal state after:
ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : ↑C
i : ι
h : ↑((π_app C fun x ↦ x ∈ {i}) a) = ↑((π_app C fun x ↦ x ∈ {i}) b)
⊢ ↑a i = ↑b i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : (iso_map C J) a = (iso_map C J) b
i : I
⊢ ↑a i = ↑b i

Tactic:
rw [Subtype.ext_iff] at h

Goal state after:
case refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : ↑((iso_map C J) a) = ↑((iso_map C J) b)
i : I
⊢ ↑a i = ↑b i