mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Valuation.Minpoly

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
Γ₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
hx : IsUnit x
⊢ v ((minpoly K x).coeff 0) ^ (finrank K L / (minpoly K x).natDegree) ≠ 0

Tactic:
have h_alg : Algebra.IsAlgebraic K L := Algebra.IsAlgebraic.of_finite K L
  have hx₀ : IsIntegral K x := (Algebra.IsAlgebraic.isAlgebraic x).isIntegral
  have hdeg := Nat.div_pos (natDegree_le x) (natDegree_pos hx₀)
  rw [ne_eq, pow_eq_zero_iff hdeg.ne.symm, Valuation.zero_iff]
  exact coeff_zero_ne_zero hx₀ hx.ne_zero

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ a = b

Tactic:
rw [Units.ext_iff, ← hr, ← ht, div_eq_div_iff, ← map_mul, ← map_mul, this.eq_iff]

Goal state after:
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ 1 (↑r * ↑u) = 1 (↑t * ↑s)

case hb
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ (valuation R) ↑s ≠ 0

case hd
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ (valuation R) ↑u ≠ 0
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Fintype.card (TruncatedWittVector p n (ZMod p)) = p ^ n

Tactic:
rw [card, ZMod.card]

Goal state after:
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ (∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (0, n + 1)) *
      (∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (1, n + 1)) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) *
            ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (1, n + 1) *
          ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      remainder p n

Tactic:
conv_rhs =>
    enter [1, 1, 2, 2]
    rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul,
      rename_C, rename_X, ← mvpz]

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ (∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (0, n + 1)) *
      (∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (1, n + 1)) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) *
            (∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
              ↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (1, n + 1) *
          ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      remainder p n
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : s.Countable
hs : ∀ x ∈ s, IsClub x
hα : cof α < ℵ₀
⊢ cof α ≤ 1

Tactic:
rwa [← cof_lt_aleph0_iff]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inl
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : s.Countable
hα : cof α < ℵ₀
⊢ cof α ≤ 1

Tactic:
rwa [← cof_lt_aleph0_iff]

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
⊢ x ≤ lfpApprox f x ↑⟨0, ⋯⟩

Tactic:
by simp [lfpApprox_zero]

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case D1
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (a : Lists α) (l : Lists' α true),
    trans a → (∀ (l' : Lists α), l' ∈ l.toList → trans l') → ∀ (l' : Lists α), l' ∈ (Lists'.cons a l).toList → trans l'

Tactic:
intro a l IH₁ IH₂
    simpa using ⟨IH₁, IH₂⟩

Goal state after:
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
h : IsOpen[inst✝³] {a}
ha : IsSuccLimit a
l u : α
h₁ : a ∈ Ioo l u
h₂ : Ioo l u ⊆ {a}
⊢ Order.succ l = a

Tactic:
simp only [mem_Ioo, subset_singleton_iff] at h₁ h₂

Goal state after:
case refine_1
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
h : IsOpen[inst✝³] {a}
ha : IsSuccLimit a
l u : α
h₁ : l < a ∧ a < u
h₂ : ∀ (y : α), l < y ∧ y < u → y = a
⊢ Order.succ l = a
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq.eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : _root_.cmp ↑n₁ ↑n₂ = Ordering.eq
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₁

Tactic:
_root_.cmp,

Goal state after:
case eq.eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : cmpUsing (fun x1 x2 ↦ x1 < x2) ↑n₁ ↑n₂ = Ordering.eq
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₁
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ 0 < veblenWith f o₂ 0

Tactic:
exact veblenWith_pos hf hp

Goal state after:
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: o : Ordinal.{u_1}
α✝ : Type u_1
A : α✝ → PSet.{u_1}
h : ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α✝ A → y.rank < o
a : α✝
⊢ succ (A a).rank ≤ o

Tactic:
rw [succ_le_iff]

Goal state after:
o : Ordinal.{u_1}
α✝ : Type u_1
A : α✝ → PSet.{u_1}
h : ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α✝ A → y.rank < o
a : α✝
⊢ (A a).rank < o
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
x : PSet.{u_1}
⊢ succ x.rank ≤ x.powerset.rank

Tactic:
rw [succ_le_iff]

Goal state after:
case a
x : PSet.{u_1}
⊢ x.rank < x.powerset.rank
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
hx : True ↔ y = x ∨ {x, y} = {x, y'}
⊢ x = x ∧ y = y'

Tactic:
true_iff

Goal state after:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
hx : y = x ∨ {x, y} = {x, y'}
⊢ x = x ∧ y = y'
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x : PSet.{u_1}
⊢ x.rank ≤ succ (⋃₀ x).rank

Tactic:
rw [← rank_powerset]
  apply rank_mono
  rw [subset_iff]
  intro z _
  rw [mem_powerset, subset_iff]
  intro _ _
  rw [mem_sUnion]
  exists z

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ε_ 0 < Γ_ o

Tactic:
by
  apply (gamma_le_gamma.2 zero_le).trans_lt'
  simpa using iterate_veblen_lt_gamma_zero 2

Goal state after:
Module: Mathlib.Tactic.Algebra.Basic

Goal state before:
pp: «$u» «$v» : Level
«$R» : Type u
«$A» : Type v
«$sR» : CommSemiring «$R»
«$sA» : CommSemiring «$A»
«$sAlg» : Algebra «$R» «$A»
$a✝ $b✝ «$a» «$b» : «$A»
«$r» «$s» «$t» : «$R»
«$pt» : «$r» * «$s» = «$t»
⊢ (algebraMap «$R» «$A») «$r» * (algebraMap «$R» «$A») «$s» = (algebraMap «$R» «$A») «$t»

Tactic:
by simp [← pt, map_mul]

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

Goal state before:
pp: case oadd
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
⊢ (a.oadd m b).FundamentalSequenceProp
    (match b.fundamentalSequence with
    | Sum.inr f => Sum.inr fun i ↦ a.oadd m (f i)
    | Sum.inl (some b') => Sum.inl (some (a.oadd m b'))
    | Sum.inl none =>
      match a.fundamentalSequence, m.natPred with
      | Sum.inl none, 0 => Sum.inl (some zero)
      | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
      | Sum.inl (some a'), 0 => Sum.inr fun i ↦ a'.oadd i.succPNat zero
      | Sum.inl (some a'), m.succ => Sum.inr fun i ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
      | Sum.inr f, 0 => Sum.inr fun i ↦ (f i).oadd 1 zero
      | Sum.inr f, m.succ => Sum.inr fun i ↦ a.oadd m.succPNat ((f i).oadd 1 zero))

Tactic:
rcases e : b.fundamentalSequence with (⟨_ | b'⟩ | f) <;>
    simp only [FundamentalSequenceProp]

Goal state after:
case oadd.inl.none
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
e : b.fundamentalSequence = Sum.inl none
⊢ match
    match a.fundamentalSequence, m.natPred with
    | Sum.inl none, 0 => Sum.inl (some zero)
    | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
    | Sum.inl (some a'), 0 => Sum.inr fun i ↦ a'.oadd i.succPNat zero
    | Sum.inl (some a'), m.succ => Sum.inr fun i ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
    | Sum.inr f, 0 => Sum.inr fun i ↦ (f i).oadd 1 zero
    | Sum.inr f, m.succ => Sum.inr fun i ↦ a.oadd m.succPNat ((f i).oadd 1 zero) with
  | Sum.inl none => a.oadd m b = 0
  | Sum.inl (some a_1) => (a.oadd m b).repr = succ a_1.repr ∧ ((a.oadd m b).NF → a_1.NF)
  | Sum.inr f =>
    IsSuccLimit (a.oadd m b).repr ∧
      (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a.oadd m b ∧ ((a.oadd m b).NF → (f i).NF)) ∧
        ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (f i).repr

case oadd.inl.some
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
b' : ONote
e : b.fundamentalSequence = Sum.inl (some b')
⊢ (a.oadd m b).repr = succ (a.oadd m b').repr ∧ ((a.oadd m b).NF → (a.oadd m b').NF)

case oadd.inr
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
f : ℕ → ONote
e : b.fundamentalSequence = Sum.inr f
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a.oadd m (f i) < a.oadd m (f (i + 1)) ∧ a.oadd m (f i) < a.oadd m b ∧ ((a.oadd m b).NF → (a.oadd m (f i)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (a.oadd m (f i)).repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
⊢ s.leadingExp = ⊥ ↔ s = nil

Tactic:
by
  cases s <;> simp

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

Goal state before:
pp: case h.cons
α : 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 : Stream'.Seq α
s_hd : α
s_tl : Stream'.Seq α
hF :
  (Seq.cons s_hd s_tl).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' s.tail))
      (h_opf.unfold s.head)
⊢ (op (Seq.cons s_hd s_tl)).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:
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.Polynomial.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
a : R
n : ℕ
⊢ Polynomial.C a * Polynomial.X ^ n = a • Polynomial.X ^ n

Tactic:
Polynomial.smul_eq_C_mul

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
a : R
n : ℕ
⊢ Polynomial.C a * Polynomial.X ^ n = Polynomial.C a * Polynomial.X ^ n
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℕ
hnm : n.blt m = true
⊢ Icc m n = ∅

Tactic:
by simpa using hnm

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℕ
s : Finset ℕ
hmn : m.ble n = true
hs : Icc (m + 1) n = s
⊢ Icc m n = insert m (Icc (m + 1) n)

Tactic:
insert_Icc_add_one_left_eq_Icc (by simpa using hmn)

Goal state after:
m n : ℕ
s : Finset ℕ
hmn : m.ble n = true
hs : Icc (m + 1) n = s
⊢ Icc m n = Icc m n
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℤ
hnm : n < m
⊢ Icc m n = ∅

Tactic:
by simpa using hnm

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℤ
s : Finset ℤ
hmn : m ≤ n
hs : Icc (m + 1) n = s
⊢ Icc m n = insert m (Icc (m + 1) n)

Tactic:
insert_Icc_add_one_left_eq_Icc (by simpa using hmn)

Goal state after:
m n : ℤ
s : Finset ℤ
hmn : m ≤ n
hs : Icc (m + 1) n = s
⊢ Icc m n = Icc m n
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) (⟨fst, snd⟩ :: m)) = List.dlookup x m

pp: case neg.a
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ x ≠ ⟨fst, snd⟩.fst

Tactic:
· simp [heq, ih]

Goal state after:
case neg.a
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ x ≠ ⟨fst, snd⟩.fst
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h : x' = x
h₃ : some y = some val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs

Tactic:
rw [Option.some_inj] at h₃
        subst x'; subst val
        simp only [List.mem_cons, true_or]

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : x ∈ xs
⊢ x = y

Tactic:
by_cases hy : y ∈ xs

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : x ∈ xs
hy : y ∈ xs
⊢ x = y

case neg
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : x ∈ xs
hy : y ∉ xs
⊢ x = y
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : x ∉ xs
⊢ x = y

Tactic:
by_cases hy : y ∈ xs

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : x ∉ xs
hy : y ∈ xs
⊢ x = y

case neg
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : x ∉ xs
hy : y ∉ xs
⊢ x = y
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case h₀
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm : map Sigma.fst (List.toFinmap' (xs₀.zip xs₁)) ~ map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))
hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup
⊢ (map Sigma.fst xs).Nodup

Tactic:
hxs,

Goal state after:
case h₀
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm : map Sigma.fst (List.toFinmap' (xs₀.zip xs₁)) ~ map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))
hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup
⊢ (map Sigma.fst (List.toFinmap' (xs₀.zip xs₁))).Nodup
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := compactCovering G
F : ℕ × ↑s → Set X := fun p ↦ (K p.1 ∩ ↑p.2 • V) • {x}
this✝ : Nonempty X
this : Encodable ↑s
n : ℕ
g : G
hg : g ∈ s
H : IsCompact ((fun g ↦ g • x) '' (K n ∩ g • V))
⊢ IsCompact (F (n, ⟨g, hg⟩))

Tactic:
by
        simpa only [F, smul_singleton] using H

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

Goal state before:
pp: X : Type u_7
Y : Type u_8
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group X
inst✝⁶ : IsTopologicalGroup X
inst✝⁵ : UniformSpace Y
inst✝⁴ : CommGroup Y
inst✝³ : IsUniformGroup Y
inst✝² : T0Space Y
inst✝¹ : CompactSpace Y
inst✝ : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : (𝓝 1).HasBasis (fun x ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : U0 ∈ 𝓝 1
U_aux : ℕ → ↑{S | S ∈ 𝓝 1} := ⋯
U : ℕ → Set X := ⋯
hU1 : ∀ (n : ℕ), U n ∈ 𝓝 1
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
hU4 : ∀ (f : X →* Y), Set.MapsTo (⇑f) (U 0) (V 0) → ∀ (n : ℕ), Set.MapsTo (⇑f) (U n) (V n)
⊢ EquicontinuousAt (fun f ↦ ⇑↑f) 1

Tactic:
rw [hVo.uniformity_of_nhds_one.equicontinuousAt_iff_right]

Goal state after:
X : Type u_7
Y : Type u_8
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group X
inst✝⁶ : IsTopologicalGroup X
inst✝⁵ : UniformSpace Y
inst✝⁴ : CommGroup Y
inst✝³ : IsUniformGroup Y
inst✝² : T0Space Y
inst✝¹ : CompactSpace Y
inst✝ : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : (𝓝 1).HasBasis (fun x ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : U0 ∈ 𝓝 1
U_aux : ℕ → ↑{S | S ∈ 𝓝 1} :=
  fun t ↦
    Nat.rec ⟨U0, hU0o⟩
      (fun x S ↦
        let h := ⋯;
        ⟨Classical.choose h, ⋯⟩)
      t
U : ℕ → Set X := fun n ↦ ↑(U_aux n)
hU1 : ∀ (n : ℕ), U n ∈ 𝓝 1
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
hU4 : ∀ (f : X →* Y), Set.MapsTo (⇑f) (U 0) (V 0) → ∀ (n : ℕ), Set.MapsTo (⇑f) (U n) (V n)
⊢ ∀ (k : ℕ), True → ∀ᶠ (x : X) in 𝓝 1, ∀ (i : ↑{f | Set.MapsTo (⇑f) (U 0) (V 0)}), (↑i 1, ↑i x) ∈ {x | x.2 / x.1 ∈ V k}
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
H : 𝓕₁ ⊓ 𝓟 V = 𝓝 0 ⊓ 𝓟 V
⊢ t₁ = t₂

Tactic:
set 𝓕₂ := @nhds E t₂ 0

Goal state after:
𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ ⊓ 𝓟 V = 𝓕₂ ⊓ 𝓟 V
⊢ t₁ = t₂
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)
⊢ IsInducing ⇑f

Tactic:
rw [isInducing_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 : IsInducing (V.domRestrict ⇑f)
⊢ inst✝⁶ = TopologicalSpace.induced (⇑f) inst✝⁵
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : CompactSpace A
V : Set (PontryaginDual A) := {ψ | Set.MapsTo (⇑ψ) Set.univ (Circle.centeredArc (π / 2))}
hVopen : IsOpen V
hVeq : V = {1}
⊢ IsOpen {1}

Tactic:
by simpa [hVeq] using hVopen

Goal state after: