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

Goal state before:
pp: case refine_2.inr
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
⊢ lfpApprox f x 0 = x

Tactic:
exact lfpApprox_zero f

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

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : f ⁻¹' Iic b = ∅
⊢ IsClosed (f ⁻¹' Iic b)

pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : (f ⁻¹' Iic b).Nonempty
⊢ IsClosed (f ⁻¹' Iic b)

Tactic:
· exact h ▸ isClosed_empty

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : (f ⁻¹' Iic b).Nonempty
⊢ IsClosed (f ⁻¹' Iic b)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝ : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF
IHe :
  match Ordering.lt, e₁, e₂ with
  | Ordering.lt, a, b => a < b
  | Ordering.eq, a, b => a = b
  | Ordering.gt, a, b => b < a
⊢ (Ordering.lt.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)

Tactic:
exact oadd_lt_oadd_1 h₁ IHe

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

Goal state before:
pp: x✝ y✝ z x y : ZFSet.{u}
hxy : x.toSet = y.toSet
⊢ ∀ (z : ZFSet.{u}), z ∈ x.toSet ↔ z ∈ y.toSet

Tactic:
intro z

Goal state after:
x✝ y✝ z✝ x y : ZFSet.{u}
hxy : x.toSet = y.toSet
z : ZFSet.{u}
⊢ z ∈ x.toSet ↔ z ∈ y.toSet
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
⊢ (a + o).NFBelow b → (e.addAux n (a + o)).NFBelow b

Tactic:
obtain - | ⟨e', n', a'⟩ := a + o

Goal state after:
case zero
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
⊢ zero.NFBelow b → (e.addAux n zero).NFBelow b

case oadd
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
⊢ (e'.oadd n' a').NFBelow b → (e.addAux n (e'.oadd n' a')).NFBelow b
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
x✝² x✝¹ : PSet.{u}
α✝ : Type u
A✝ : α✝ → PSet.{u}
x✝ : ⟦x✝¹⟧ ∈ ⟦PSet.mk α✝ A✝⟧
a : (PSet.mk α✝ A✝).Type
ya : x✝¹.Equiv ((PSet.mk α✝ A✝).Func a)
⊢ f ⟦x✝¹⟧ ∈ image f ⟦PSet.mk α✝ A✝⟧

Tactic:
simp only [mk_eq, ← Definable₁.mk_out (f := f)]

Goal state after:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
x✝² x✝¹ : PSet.{u}
α✝ : Type u
A✝ : α✝ → PSet.{u}
x✝ : ⟦x✝¹⟧ ∈ ⟦PSet.mk α✝ A✝⟧
a : (PSet.mk α✝ A✝).Type
ya : x✝¹.Equiv ((PSet.mk α✝ A✝).Func a)
⊢ ZFSet.mk (Definable₁.out f x✝¹) ∈ image f (ZFSet.mk (PSet.mk α✝ A✝))
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x : PSet.{u_1}
⊢ ∀ ⦃z : PSet.{u_1}⦄, z ∈ x → z ∈ (⋃₀ x).powerset

Tactic:
intro z

Goal state after:
x z : PSet.{u_1}
⊢ z ∈ x → z ∈ (⋃₀ x).powerset
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x : ZFSet.{u_1}
⊢ x ⊆ (⋃₀ x).powerset

Tactic:
intro z

Goal state after:
x z : ZFSet.{u_1}
⊢ z ∈ x → z ∈ (⋃₀ x).powerset
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
⊢ Class.ToSet (fun x_1 ↦ ↑(map f x) (x_1.pair z)) ↑y ↔ z = f y

Tactic:
Class.toSet_of_ZFSet,

Goal state after:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
⊢ ↑(map f x) (y.pair z) ↔ z = f y
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case mp
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
⊢ x = y ∨ x ∈ y

Tactic:
by_cases hyx : y ⊆ x

Goal state after:
case pos
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : y ⊆ x
⊢ x = y ∨ x ∈ y

case neg
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
⊢ x = y ∨ x ∈ y
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
m : ZFSet.{u}
hm : m ∈ ↑y \ ↑x
hm' : ∀ x_1 ∈ ↑y \ ↑x, x_1 ∉ m
hmy : m ∈ y
⊢ m ⊆ x

Tactic:
intro z

Goal state after:
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
m : ZFSet.{u}
hm : m ∈ ↑y \ ↑x
hm' : ∀ x_1 ∈ ↑y \ ↑x, x_1 ∉ m
hmy : m ∈ y
z : ZFSet.{u}
⊢ z ∈ m → z ∈ x
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
m : ZFSet.{u}
hm : m ∈ ↑y \ ↑x
hm' : ∀ x_1 ∈ ↑y \ ↑x, x_1 ∉ m
hmy : m ∈ y
z : ZFSet.{u}
hzm : z ∈ m
⊢ z ∈ x

Tactic:
by_contra hzx

Goal state after:
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
m : ZFSet.{u}
hm : m ∈ ↑y \ ↑x
hm' : ∀ x_1 ∈ ↑y \ ↑x, x_1 ∉ m
hmy : m ∈ y
z : ZFSet.{u}
hzm : z ∈ m
hzx : z ∉ x
⊢ False
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ∉ b₂ → b₂ ⊆ a₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hyx : x ∉ y
z : ZFSet.{u}
hzy : z ∈ y
⊢ z ∈ x

Tactic:
by_contra hzx

Goal state after:
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ∉ b₂ → b₂ ⊆ a₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hyx : x ∉ y
z : ZFSet.{u}
hzy : z ∈ y
hzx : z ∉ x
⊢ False
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: o : Ordinal.{u}
x : ZFSet.{u}
⊢ x ∈ V_ o ↔ ∃ a < o, x ⊆ V_ a

Tactic:
by rw [vonNeumann]; simp

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ⨆ a, Order.succ (↑a.toOrd).toPSet.rank = o

Tactic:
conv_rhs => rw [← _root_.iSup_succ o]

Goal state after:
o : Ordinal.{u_1}
⊢ ⨆ a, Order.succ (↑a.toOrd).toPSet.rank = ⨆ a, Order.succ ↑a
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a.toZFSet ∈ b.toZFSet ↔ a < b

Tactic:
refine ⟨?_, toZFSet_mem_toZFSet_of_lt⟩

Goal state after:
a b : Ordinal.{u_1}
⊢ a.toZFSet ∈ b.toZFSet → a < b
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
⊢ (e.opowAux a0 a (k + 1) m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr

Tactic:
by
    by_cases h : m = 0 <;> simp only [h, opowAux, mulNat_eq_mul, repr_add, repr_scale, repr_mul,
      repr_ofNat, zero_add, mul_add, repr_zero, mul_zero, scale_opowAux e, opow_add, mul_assoc]

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

Goal state before:
pp: case h
f g : ℝ → ℝ
a b : ℝ
hf : ∀ᶠ (x : ℝ) in atTop, 0 < f x
hg : Tendsto g atTop atTop
h : (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hb : 0 < b
⊢ Tendsto (b • Real.log ∘ g - a • Real.log ∘ f) atTop atTop

Tactic:
have h' : (b • Real.log ∘ g - a • Real.log ∘ f) ~[atTop] b • Real.log ∘ g := by
    replace h : (a • Real.log ∘ f) =o[atTop] (b • Real.log ∘ g) :=
      (h.const_mul_left a).const_mul_right (hb.ne')
    grind only [IsEquivalent.sub_isLittleO, IsEquivalent.refl]

Goal state after:
case h
f g : ℝ → ℝ
a b : ℝ
hf : ∀ᶠ (x : ℝ) in atTop, 0 < f x
hg : Tendsto g atTop atTop
h : (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hb : 0 < b
h' : b • Real.log ∘ g - a • Real.log ∘ f ~[atTop] b • Real.log ∘ g
⊢ Tendsto (b • Real.log ∘ g - a • Real.log ∘ f) atTop atTop
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons
hd : ℝ
tl : List ℝ
ih :
  ∀ {basis_hd : ℝ → ℝ} {basis_tl : Basis},
    tl.length = List.length basis_tl → WellFormedBasis (basis_hd :: basis_tl) → Majorized (toFun tl basis_tl) basis_hd 0
basis_hd basis_tl_hd : ℝ → ℝ
basis_tl_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl_hd :: basis_tl_tl)
h_length : tl.length = basis_tl_tl.length
⊢ Majorized (basis_tl_hd ^ hd * toFun tl basis_tl_tl) basis_hd (0 + 0)

Tactic:
apply Majorized.mul (h_basis.tail_pow_majorized_head (by simp) _) _
        h_basis.head_eventually_pos

Goal state after:
hd : ℝ
tl : List ℝ
ih :
  ∀ {basis_hd : ℝ → ℝ} {basis_tl : Basis},
    tl.length = List.length basis_tl → WellFormedBasis (basis_hd :: basis_tl) → Majorized (toFun tl basis_tl) basis_hd 0
basis_hd basis_tl_hd : ℝ → ℝ
basis_tl_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl_hd :: basis_tl_tl)
h_length : tl.length = basis_tl_tl.length
⊢ Majorized (toFun tl basis_tl_tl) basis_hd 0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons.cons.rel.h.h_firstIsPos
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
exp2 : ℝ
m2 : List ℝ
h : exp1 < exp2
h1 : m1.length = basis_tl.length
h2 : m2.length = basis_tl.length
⊢ FirstNonzeroIsPos ((exp2 - exp1) :: mul m2 (inv m1))

Tactic:
apply FirstNonzeroIsPos.of_head
        grind

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

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

Tactic:
UnitMonomial.inv_toFun h_basis

Goal state after:
t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
⊢ t.coef⁻¹ • (t.unit.toFun basis)⁻¹ =ᶠ[atTop] (t.coef • t.unit.toFun basis)⁻¹
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : (Nat.unpair n).1 = 0
⊢ (S.nat (Nat.unpair n).2).encode = n

Tactic:
unfold S.encode

Goal state after:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : (Nat.unpair n).1 = 0
⊢ Nat.pair 0 (Nat.unpair n).2 = n
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
⊢ ((S.decode ((Nat.unpair n).1 - 1)).cons (S.decode (Nat.unpair n).2)).encode = n

Tactic:
unfold S.encode

Goal state after:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
⊢ Nat.pair ((S.decode ((Nat.unpair n).1 - 1)).encode + 1) (S.decode (Nat.unpair n).2).encode = n
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a : ℤ
b ab' : ℕ
ab r b' : ℤ
hb' : ↑b = b'
hab : a % b' = ab
h : ↑ab' = ab
hr : jacobiSymNat ab' b = r
⊢ jacobiSym ab b = jacobiSym (↑ab') b

Tactic:
← h

Goal state after:
a : ℤ
b ab' : ℕ
ab r b' : ℤ
hb' : ↑b = b'
hab : a % b' = ab
h : ↑ab' = ab
hr : jacobiSymNat ab' b = r
⊢ jacobiSym (↑ab') b = jacobiSym (↑ab') b
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos
α : 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 (⟨fst, snd⟩ :: m)

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 (⟨fst, snd⟩ :: m)

Tactic:
· simp [heq]

Goal state after:
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 (⟨fst, snd⟩ :: m)
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case cons.zero
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
h₂ : (x' :: xs)[0]? = some x
⊢ applyId ((x' :: xs).zip ys) x = y ↔ ys[0]? = some y

pp: case cons.succ
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
⊢ applyId ((x' :: xs).zip ys) x = y ↔ ys[n✝ + 1]? = some y

Tactic:
· simp only [length_cons, lt_add_iff_pos_left, add_pos_iff, Nat.lt_add_one, or_true,
        getElem?_eq_getElem, getElem_cons_zero, Option.some.injEq] at h₂
      subst h₂
      cases ys
      · cases h₁
      · simp

Goal state after:
case cons.succ
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
⊢ applyId ((x' :: xs).zip ys) x = y ↔ ys[n✝ + 1]? = some y
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ (dlookup x (map Prod.toSigma (xs.zip ys))).getD x = x

Tactic:
rw [List.dlookup_eq_none.2]

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ none.getD x = x

α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ x ∉ (map Prod.toSigma (xs.zip ys)).keys
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}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, ⟨g, hg⟩))).Nonempty
I : (interior ((g • V) • {x})).Nonempty
y : X
hy : y ∈ interior (V • {x})
⊢ ∃ g' ∈ V, g' • x = y

Tactic:
by simpa using interior_subset hy

Goal state after:
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
x : X
g : G
U : Set G
hU : U ∈ 𝓝 g
⊢ (fun x_1 ↦ x_1 • x) = (fun x_1 ↦ x_1 • g • x) ∘ fun x ↦ x * g⁻¹

Tactic:
ext g

Goal state after:
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
x : X
g✝ : G
U : Set G
hU : U ∈ 𝓝 g✝
g : G
⊢ g • x = ((fun x_1 ↦ x_1 • g✝ • x) ∘ fun x ↦ x * g✝⁻¹) g
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 : ∀ (s : Set X.A), x ∈ s → IsOpen s → s ∈ ↑F
A : Set X.A
hA : IsClosed A
h : A ∈ F
H : x ∉ A
⊢ False

Tactic:
specialize cond Aᶜ H hA.isOpen_compl

Goal state after:
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
A : Set X.A
cond : Aᶜ ∈ ↑F
hA : IsClosed A
h : A ∈ F
H : x ∉ A
⊢ False
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝³ : (i : I) → Decidable (J i)
inst✝² : (i : I) → Decidable (K i)
inst✝¹ : (i : I) → Decidable (L i)
inst✝ : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
X✝ Y✝ Z✝ : (Finset I)ᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := ProjRestricts C ⋯, continuous_toFun := ⋯ } =
    CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := ProjRestricts C ⋯, continuous_toFun := ⋯ } ≫
      CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := ProjRestricts C ⋯, continuous_toFun := ⋯ }

Tactic:
by rw [← CompHausLike.ofHom_comp]; congr; dsimp; rw [projRestricts_eq_comp]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case inl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne : ⟨a, ha⟩ ≠ ⟨b, hb⟩
h' : ⟨a, ha⟩ < ⟨b, hb⟩
⊢ Products.eval C b ∈ Submodule.span ℤ (Products.eval C '' {m | m < b})

Tactic:
← h

Goal state after:
case inl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne : ⟨a, ha⟩ ≠ ⟨b, hb⟩
h' : ⟨a, ha⟩ < ⟨b, hb⟩
⊢ Products.eval C a ∈ Submodule.span ℤ (Products.eval C '' {m | m < b})
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: D : CompHaus
x✝ : Set ↑D.1
h : IsOpen x✝
⊢ IsOpen (id ⁻¹' x✝)

Tactic:
by
          rw [isOpen_iff_ultrafilter'] at h
          exact h

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun x ↦ ord I x < o) l
⊢ ∀ b ∈ ↑l, Order.succ (ord I b) < o

Tactic:
exact fun b hb ↦ ho.succ_lt (prop_of_isGood C (ord I · < o) h b hb)

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
h : ∀ o' < o, P I o'
hho : o ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
⊢ IsClosed C → contained C o → LinearIndependent ℤ (eval C)

Tactic:
hC

Goal state after:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
h : ∀ o' < o, P I o'
hho : o ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
⊢ contained C o → LinearIndependent ℤ (eval C)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ ↑E ⊆ C

Tactic:
simp_rw [← union, ← RelCWComplex.union_iUnion_openCell_eq_complex]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ D ∪ ⋃ n, ⋃ j, openCell n ↑j ⊆ D ∪ ⋃ n, ⋃ j, openCell n j
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
C : ℕ → Set α
⊢ (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, dissipate C n = ∅

Tactic:
hC

Goal state after:
α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
C : ℕ → Set α
hC : ∀ (i : ℕ), C i ∈ S
⊢ ⋂ i, C i = ∅ → ∃ n, dissipate C n = ∅
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
M0 : 0 < M
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

Tactic:
refine ⟨fun hn x ↦ lt_of_le_of_lt (norm_coe_le_norm f x) hn, ?_⟩
  · obtain (he | he) := isEmpty_or_nonempty α
    · simpa
    · obtain ⟨x, hx⟩ := exist_norm_eq h
      exact fun h ↦ hx ▸ h x

Goal state after:
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

Tactic:
obtain (hM | hM) := lt_or_ge 0 M
  · exact norm_lt_iff_of_compactlySupported h hM
  · exact ⟨fun h ↦ False.elim <| (h.trans_le hM).not_ge (by positivity),
      fun h ↦ False.elim <| (h (Classical.arbitrary α) |>.trans_le hM).not_ge (by positivity)⟩

Goal state after:
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝² : TopologicalSpace E
A : Set E
inst✝¹ : Countable ι
inst✝ : Nonempty ι
hA : IsCountablyCompact A
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst✝²] (U i)
hAU : A ⊆ ⋃ i, U i
hdU : Directed (fun x1 x2 ↦ x1 ⊆ x2) U
h : ∀ (i : ι), ¬A ⊆ U i
hdir : Directed (fun x1 x2 ↦ x1 ≥ x2) fun i ↦ 𝓟 (A \ U i)
⊢ False

Tactic:
have : NeBot (⨅ i, 𝓟 (A \ U i)) :=
    iInf_neBot_of_directed' hdir fun i => (sdiff_nonempty.mpr (h i)).principal_neBot

Goal state after:
ι : Type u_1
E : Type u_2
inst✝² : TopologicalSpace E
A : Set E
inst✝¹ : Countable ι
inst✝ : Nonempty ι
hA : IsCountablyCompact A
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst✝²] (U i)
hAU : A ⊆ ⋃ i, U i
hdU : Directed (fun x1 x2 ↦ x1 ⊆ x2) U
h : ∀ (i : ι), ¬A ⊆ U i
hdir : Directed (fun x1 x2 ↦ x1 ≥ x2) fun i ↦ 𝓟 (A \ U i)
this : (⨅ i, 𝓟 (A \ U i)).NeBot
⊢ False