mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
⊢ ⨆ i ∈ ∅, g i = ⨆ x ∈ ∅, g (f x)

Tactic:
cbiSup_empty,

Goal state after:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
⊢ sSup ∅ = ⨆ x ∈ ∅, g (f x)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
⊢ sSup ∅ = ⨆ x ∈ ∅, g (f x)

Tactic:
cbiSup_empty

Goal state after:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
⊢ sSup ∅ = sSup ∅
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
hg : ¬BddAbove (range g)
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)

Tactic:
ciSup_of_not_bddAbove hg,

Goal state after:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
hg : ¬BddAbove (range g)
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (sSup ∅)
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ Icc a b = {a, b}

Tactic:
ext c

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
c : α
⊢ c ∈ Icc a b ↔ c ∈ {a, b}
Module: Mathlib.Data.Set.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

Tactic:
by_cases h₁ : x.1 ∈ s₁ <;> by_cases h₂ : x.2 ∈ t₁ x.1

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∈ s₁
h₂ : x.snd ∈ t₁ x.fst
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

case neg
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∈ s₁
h₂ : x.snd ∉ t₁ x.fst
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

case pos
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∉ s₁
h₂ : x.snd ∈ t₁ x.fst
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

case neg
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∉ s₁
h₂ : x.snd ∉ t₁ x.fst
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
x y : α
⊢ x = y ∨ x ⋖ y ↔ ReflGen (fun x1 x2 ↦ x1 ⋖ x2) x y

Tactic:
@eq_comm _ x,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
x y : α
⊢ y = x ∨ x ⋖ y ↔ ReflGen (fun x1 x2 ↦ x1 ⋖ x2) x y
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
⊢ e (⨆ i, f i) = ⨆ i, e (f i)

Tactic:
cases isEmpty_or_nonempty ι
  · simp [map_bot]
  by_cases hf : BddAbove (range f)
  · exact e.map_ciSup hf
  · have hfe : ¬ BddAbove (range fun i ↦ e (f i)) := by
      simpa [Set.Nonempty, BddAbove, upperBounds, e.surjective.forall] using hf
    simp [map_bot, hf, hfe]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι), a x < c x → c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
c : (i : ι) → α i := Function.update a i (b i)
h₁ : c ≤ b
⊢ a i < c i

Tactic:
simpa [c]

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

Goal state before:
pp: case inl.mp
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ ∀ x_1 ∈ f a b, ⟨i, x_1⟩ = x → ∃ (h : i = x.fst) (h_1 : i = x.fst), x.snd ∈ f (⋯ ▸ a) (⋯ ▸ b)

Tactic:
rintro x hx rfl

Goal state after:
case inl.mp
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
hx : x ∈ f a b
⊢ ∃ (h : i = ⟨i, x⟩.fst) (h_1 : i = ⟨i, x⟩.fst), ⟨i, x⟩.snd ∈ f (⋯ ▸ a) (⋯ ▸ b)
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ (sigmaLift f a b).Nonempty ↔ ∃ (h : a.fst = b.fst), (f (h ▸ a.snd) b.snd).Nonempty

Tactic:
nonempty_iff_ne_empty,

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ sigmaLift f a b ≠ ∅ ↔ ∃ (h : a.fst = b.fst), f (⋯ ▸ a.snd) b.snd ≠ ∅
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
⊢ WellQuasiOrdered r ↔ ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
constructor <;> intro h f
  · exact h.exists_monotone_subseq f
  · obtain ⟨g, gmon⟩ := h f
    exact ⟨_, _, g.strictMono Nat.zero_lt_one, gmon _ _ (Nat.zero_le 1)⟩

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
⊢ (range f).WellFoundedOn r ↔ WellFounded (r on f)

Tactic:
let f' : β → range f := fun c => ⟨f c, c, rfl⟩
  refine ⟨fun h => (InvImage.wf f' h).mono fun c c' => id, fun h => ⟨?_⟩⟩
  rintro ⟨_, c, rfl⟩
  refine Acc.of_downward_closed f' ?_ _ ?_
  · rintro _ ⟨_, c', rfl⟩ -
    exact ⟨c', rfl⟩
  · exact h.apply _

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
a b : α
h : a < b
x✝ : Finset α
hs : Icc a b = x✝
⊢ False

Tactic:
induction hs : Finset.Icc a b using Finset.strongInduction generalizing b with

Goal state after:
case H
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
a : α
i : Finset α
ih : ∀ t ⊂ i, ∀ (b : α), a < b → Icc a b = t → False
b : α
h : a < b
hs : Icc a b = i
⊢ False
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
h : a ∈ orbit (↥H) b
⊢ ↑a ∈ orbit ↥H ↑b

pp: case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
h : ↑a ∈ orbit ↥H ↑b
⊢ a ∈ orbit (↥H) b

Tactic:
· rcases h with ⟨g, rfl⟩
    exact MulAction.mem_orbit _ g

Goal state after:
case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
h : ↑a ∈ orbit ↥H ↑b
⊢ a ∈ orbit (↥H) b
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
hs : s.IsPWO
ha : a ∈ s
t : Set ↑s := {x | ↑x ≤ a}
h : t.Nonempty := Exists.intro ⟨a, ha⟩ le_rfl
y : α
hy : (fun x ↦ x ∈ s) y
hle : y ≤ ↑(⋯.min t h)
hnle : ¬↑(⋯.min t h) ≤ y
⊢ False

Tactic:
exact hs.wellFounded.not_lt_min t (x := ⟨y, hy⟩) (hle.trans (hs.wellFounded.min_mem t h))
    ⟨hle, hnle⟩

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
h : a ∈ MulAction.orbit (↥H) b
⊢ ↑a ∈ MulAction.orbit ↥H ↑b

Tactic:
· rcases h with ⟨g, rfl⟩
    exact MulAction.mem_orbit _ g

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
hc : ∀ (n : ℕ), ¬(ofLex f (g 0)).1 < (ofLex f (g n)).1
⊢ ∃ m n, m < n ∧ f m ≤ f n

Tactic:
have hhc : ∀ n, (ofLex f (g 0)).1 = (ofLex f (g n)).1 := by
      intro n
      exact (hhg n).eq_of_not_lt (hc n)

Goal state after:
case neg
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
hc : ∀ (n : ℕ), ¬(ofLex f (g 0)).1 < (ofLex f (g n)).1
hhc : ∀ (n : ℕ), (ofLex f (g 0)).1 = (ofLex f (g n)).1
⊢ ∃ m n, m < n ∧ f m ≤ f n
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
S : Set G
N : Subgroup G
hLE : S ⊆ ↑(normalizer ↑N)
⊢ ⋃ a ∈ S, {x | a⁻¹ * x ∈ ↑N} = ⋃ a ∈ S, {x | x * a⁻¹ ∈ ↑N}

Tactic:
congr! 5 with s hs x

Goal state after:
case f
G : Type u_2
inst✝ : Group G
S : Set G
N : Subgroup G
hLE : S ⊆ ↑(normalizer ↑N)
s : G
hs : s ∈ S
x : G
⊢ s⁻¹ * x ∈ ↑N ↔ x * s⁻¹ ∈ ↑N
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
S : Set G
N : Subgroup G
hLE : S ⊆ ↑(normalizer ↑N)
⊢ S * ↑N = ↑N * S

Tactic:
rw [← iUnion_mul_left_image, ← iUnion_mul_right_image]
  simp only [image_mul_left, image_mul_right, Set.preimage]
  congr! 5 with s hs x
  exact (mem_normalizer_iff'.mp (inv_mem (hLE hs)) x).symm

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

Goal state before:
pp: ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ (↑univ).Pairwise (Commute on fun i ↦ (MonoidHom.mulSingle M i) (x i))

Tactic:
intro i _ j _ _
    exact Pi.mulSingle_apply_commute x i j

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq M
m : Multiset M
s : Finset M
l : List M
⊢ (↑l).toFinset ⊆ s → l.prod = ∏ x ∈ s, x ^ List.count x l

Tactic:
apply prod_list_count_of_subset l s

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group G
inst✝¹ : Group H
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst✝ : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
⊢ (map N M f h).ker = Subgroup.map (mk' N) (Subgroup.comap f M)

Tactic:
simp_rw [← ker_mk' M, MonoidHom.comap_ker]
  exact QuotientGroup.ker_lift _ _ _

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : a ∈ s
h : x = a
⊢ f a = 1

Tactic:
← prod_subset (singleton_subset_iff.2 hx) fun t ht ha => h1 t ht (notMem_singleton.1 ha),

Goal state after:
case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ {a}, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : a ∈ s
h : x = a
⊢ f a = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ ∏ i ∈ range n, f (i + 1) / f i = f n / f 0

Tactic:
apply prod_range_induction

Goal state after:
case base
G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ f 0 / f 0 = 1

case step
G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ ∀ k < n, f (k + 1) / f 0 = f k / f 0 * (f (k + 1) / f k)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ ∏ i ∈ range n, f i / f (i + 1) = f 0 / f n

Tactic:
apply prod_range_induction

Goal state after:
case base
G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ f 0 / f 0 = 1

case step
G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ ∀ k < n, f 0 / f (k + 1) = f 0 / f k * (f k / f (k + 1))
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Normal
h₂ : H₂.Normal
⊢ ⁅H₁, H₂⁆.Normal

Tactic:
let base : Set G := { x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x }
  change (closure base).Normal
  suffices h_base : base = Group.conjugatesOfSet base by
    rw [h_base]
    exact Subgroup.normalClosure_normal
  refine Set.Subset.antisymm Group.subset_conjugatesOfSet fun a h => ?_
  simp_rw [Group.mem_conjugatesOfSet_iff, isConj_iff] at h
  rcases h with ⟨b, ⟨c, hc, e, he, rfl⟩, d, rfl⟩
  exact ⟨_, h₁.conj_mem c hc d, _, h₂.conj_mem e he d, (conjugate_commutatorElement c e d).symm⟩

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
x✝ : ∃ c, ↑c * x = ↑c * y
c : ↥S
h : f ↑c * f x = f ↑c * f y
⊢ f x = f y

Tactic:
exact (f.map_units c).mul_right_inj.mp h

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
f : S.LocalizationMap N
P : Type u_4
inst✝ : Monoid P
j k : N →* P
n : N
m : M
s : ↥S
hn : n * f ↑s = f m
h : ∀ (a : M), j (f a) = k (f a)
⊢ j (n * f ↑s) = k n * k (f ↑s)

Tactic:
← k.map_mul,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
f : S.LocalizationMap N
P : Type u_4
inst✝ : Monoid P
j k : N →* P
n : N
m : M
s : ↥S
hn : n * f ↑s = f m
h : ∀ (a : M), j (f a) = k (f a)
⊢ j (n * f ↑s) = k (n * f ↑s)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
⊢ mk a₁ a₂ = mk b₁ b₂ ↔ ↑b₂ * a₁ = ↑a₂ * b₁

Tactic:
simp_rw [mk_eq_mk_iff, r_iff_exists, mul_left_cancel_iff, exists_const]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.coe.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
ha : ¬↑a✝ = 0
hb : ¬⊤ = 0
⊢ untopD 0 (↑a✝ * ⊤) = untopD 0 ↑a✝ * untopD 0 ⊤

Tactic:
rw [mul_top ha, untopD_top, mul_zero]

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹² : Monoid M
S : Submonoid M
inst✝¹¹ : OreSet S
inst✝¹⁰ : MulAction M X
inst✝⁹ : SMul R X
inst✝⁸ : SMul R M
inst✝⁷ : IsScalarTower R M M
inst✝⁶ : IsScalarTower R M X
inst✝⁵ : SMul R' X
inst✝⁴ : SMul R' M
inst✝³ : IsScalarTower R' M M
inst✝² : IsScalarTower R' M X
inst✝¹ : SMul R R'
inst✝ : IsScalarTower R R' M
r : R
m : R'
x : OreLocalization S X
⊢ ((r • m) • 1 /ₒ 1) • x = (r • 1 * m • 1 /ₒ 1) • x

Tactic:
simp only [smul_mul_assoc, smul_assoc, one_mul]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ici (succ a) ∩ Iic b = Ioc a b

Tactic:
Ici_succ_of_not_isMax ha,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ioi a ∩ Iic b = Ioc a b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ici (succ a) ∩ Iio b = Ioo a b

Tactic:
Ici_succ_of_not_isMax ha,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ioi a ∩ Iio b = Ioo a b
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
⊢ (∃ x, succ x = a) ↔ a ∈ range succ

Tactic:
mem_range

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : PartialOrder β
inst✝ : SuccOrder β
f : α ≃o β
a : α
h : IsMax a
⊢ f (succ a) = succ (f a)

Tactic:
h.succ_eq,

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : PartialOrder β
inst✝ : SuccOrder β
f : α ≃o β
a : α
h : IsMax a
⊢ f a = succ (f a)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
⊢ a ≤ succ b ↔ a = succ b ∨ a ≤ b

Tactic:
by
  by_cases hb : IsMax b
  · rw [hb.succ_eq, or_iff_right_of_imp le_of_eq]
  · rw [← lt_succ_iff_of_not_isMax hb, le_iff_eq_or_lt]

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

Goal state before:
pp: n : ℕ∞
hn0 : n ≠ 0
hxt : n ≠ ⊤
⊢ ¬n = 0 ∧ ¬n = ⊤

Tactic:
exact ⟨hn0, hxt⟩

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

Goal state before:
pp: case pos
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
i : ι
p : π i → Prop
hf : p (f i)
hg : p (g i)
hi : i ∈ s
⊢ p (s.piecewise f g i)

Tactic:
simpa [hi]

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

Goal state before:
pp: case neg
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
i : ι
p : π i → Prop
hf : p (f i)
hg : p (g i)
hi : i ∉ s
⊢ p (s.piecewise f g i)

Tactic:
simpa [hi]

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

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
hi : i ∈ s
v : π i
⊢ s.piecewise (update f i v) (update g i v) = s.piecewise (update f i v) g

Tactic:
refine s.piecewise_congr (fun _ _ => rfl) fun j hj => update_of_ne ?_ ..

Goal state after:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
hi : i ∈ s
v : π i
j : ι
hj : j ∉ s
⊢ j ≠ i
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f g : (i : ι) → π i
⊢ (univ.erase i).piecewise f g = update f i (g i)

Tactic:
by
  rw [← compl_singleton, piecewise_compl, piecewise_singleton]

Goal state after:
Module: Mathlib.Control.Traversable.Basic

Goal state before:
pp: case mk
F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
η' : ApplicativeTransformation F G
app✝ : (α : Type u) → F α → G α
preserves_pure'✝ : ∀ {α : Type u} (x : α), app✝ α (pure x) = pure x
preserves_seq'✝ : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app✝ β (x <*> y) = app✝ (α → β) x <*> app✝ α y
h :
  (fun {α} ↦ { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ }.app α) = fun {α} ↦
    η'.app α
⊢ { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ } = η'

Tactic:
cases η'

Goal state after:
case mk.mk
F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
app✝¹ : (α : Type u) → F α → G α
preserves_pure'✝¹ : ∀ {α : Type u} (x : α), app✝¹ α (pure x) = pure x
preserves_seq'✝¹ : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app✝¹ β (x <*> y) = app✝¹ (α → β) x <*> app✝¹ α y
app✝ : (α : Type u) → F α → G α
preserves_pure'✝ : ∀ {α : Type u} (x : α), app✝ α (pure x) = pure x
preserves_seq'✝ : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app✝ β (x <*> y) = app✝ (α → β) x <*> app✝ α y
h :
  (fun {α} ↦ { app := app✝¹, preserves_pure' := preserves_pure'✝¹, preserves_seq' := preserves_seq'✝¹ }.app α) =
    fun {α} ↦ { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ }.app α
⊢ { app := app✝¹, preserves_pure' := preserves_pure'✝¹, preserves_seq' := preserves_seq'✝¹ } =
    { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ }
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
⊢ ∃ g, ∀ i ∈ insert a s, ↑(g i) = f i

Tactic:
have hfs' : Set.InjOn f s := hfs.mono (s.subset_insert a)

Goal state after:
case insert
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
⊢ ∃ g, ∀ i ∈ insert a s, ↑(g i) = f i
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := s.toFinset
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f ↑s'
g : α ≃ ↥t
hg : ∀ i ∈ s', ↑(g i) = f i
⊢ ∃ g, ∀ i ∈ s, ↑(g i) = f i

Tactic:
refine ⟨g, fun i hi => ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := s.toFinset
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f ↑s'
g : α ≃ ↥t
hg : ∀ i ∈ s', ↑(g i) = f i
i : α
hi : i ∈ s
⊢ ↑(g i) = f i
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
e : α ≃ β
x : Sym α n
⊢ map (⇑e.symm) (map (⇑e) x) = x

Tactic:
map_map,

Goal state after:
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
e : α ≃ β
x : Sym α n
⊢ map (⇑e.symm ∘ ⇑e) x = x
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
e : α ≃ β
x : Sym β n
⊢ map (⇑e) (map (⇑e.symm) x) = x

Tactic:
map_map,

Goal state after:
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
e : α ≃ β
x : Sym β n
⊢ map (⇑e ∘ ⇑e.symm) x = x
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
l : List α
⊢ decodeList (encodeList l) = some l

Tactic:
induction l

Goal state after:
case nil
α : Type u_1
inst✝ : Encodable α
⊢ decodeList (encodeList []) = some []

case cons
α : Type u_1
inst✝ : Encodable α
head✝ : α
tail✝ : List α
tail_ih✝ : decodeList (encodeList tail✝) = some tail✝
⊢ decodeList (encodeList (head✝ :: tail✝)) = some (head✝ :: tail✝)
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case neg
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ (v.set i a).get j = v.get j

Tactic:
rwa [get_set_of_ne]

Goal state after:
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: case inl.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : ¬r x a
b : α
hb : r x b
⊢ r (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inl ⟨a, ha⟩))
      (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ ¬r x x_1) (Subrel r (r x)) (Sum.inl ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)

Tactic:
simpa using trans_trichotomous_left ha hb

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
c : β
ha : inr a < inr c
hb : inr c < inr b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
exact ⟨c, inr_lt_inr_iff.1 ha, inr_lt_inr_iff.1 hb⟩

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: x : Cardinal.{u_1}
h : x ≠ 0
⊢ Nonempty (Quotient.out x)

Tactic:
← mk_ne_zero_iff,

Goal state after:
x : Cardinal.{u_1}
h : x ≠ 0
⊢ #(Quotient.out x) ≠ 0