mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ ∀ ⦃a : (x : ι) × α x⦄, a ∈ map (Embedding.sigmaMk i) (t i) → a ∉ map (Embedding.sigmaMk j) (t j)

Tactic:
mem_map,

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ ∀ ⦃a : (x : ι) × α x⦄, (∃ a_1 ∈ t i, (Embedding.sigmaMk i) a_1 = a) → ¬∃ a_2 ∈ t j, (Embedding.sigmaMk j) a_2 = a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrder α
⊢ Ico a b ⊆ Ici a

Tactic:
by
  simpa [← coe_subset] using Set.Ico_subset_Ici_self

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 : α
a b : ↑(orbit G x)
g : ↥H
h : ↑(↑g • b) = ↑a
⊢ a ∈ orbit (↥H) b

Tactic:
← Subtype.ext_iff

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)
g : ↥H
h : ↑g • b = a
⊢ a ∈ orbit (↥H) b
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 : Quotient G α
a b : ↑x.orbit
g : ↥H
h : ↑(↑g • b) = ↑a
⊢ a ∈ MulAction.orbit (↥H) b

Tactic:
← Subtype.ext_iff

Goal state after:
case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
g : ↥H
h : ↑g • b = a
⊢ a ∈ MulAction.orbit (↥H) b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ c < a → c < b → ¬(min a b ≤ c ∧ c ≤ max a b)

Tactic:
exact Set.notMem_uIcc_of_lt

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

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

Tactic:
mem_orbit_symm (a₂ := c)

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
⊢ c ∈ MulAction.orbit ↥H ↑a ↔ c ∈ MulAction.orbit ↥H ↑b
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
a : α
m : G
ha : m • a = a
⊢ m⁻¹ • a = a

Tactic:
rw [inv_smul_eq_iff, ha]

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
S : Set M
inst✝ : Semigroup M
h : ⊤ ⊆ S.centralizer
x✝¹ : M
hx : x✝¹ ∈ S
x✝ : M
⊢ x✝ * x✝¹ = x✝¹ * x✝

Tactic:
h trivial _ hx

Goal state after:
M : Type u_1
S : Set M
inst✝ : Semigroup M
h : ⊤ ⊆ S.centralizer
x✝¹ : M
hx : x✝¹ ∈ S
x✝ : M
⊢ x✝ * x✝¹ = x✝ * x✝¹
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : Mˣ
ha : ∀ (g : M), g * ↑a = ↑a * g
⊢ ∀ (g : M), g * ↑a⁻¹ = ↑a⁻¹ * g

Tactic:
exact (Commute.units_inv_right <| ha ·)

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case inv_mem
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x✝ : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ i, ↑(S i)
⊢ C x⁻¹

Tactic:
| inv_mem x hx =>

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case inv_mem
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x✝ x : G
hx : x ∈ ↑H * ↑N
⊢ x⁻¹ ∈ ↑H * ↑N

Tactic:
| inv_mem x hx =>

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
⊢ ∏ k ∈ range 0, f k = 1

Tactic:
by rw [range_zero, prod_empty]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
⊢ H.normalCore = ⨅ g, g • H

Tactic:
ext g

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
g : G
⊢ g ∈ H.normalCore ↔ g ∈ ⨅ g, g • H
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
g : G
⊢ ConjAct.toConjAct g • H = H ↔ g⁻¹ ∈ normalizer ↑H

Tactic:
simp only [Subgroup.ext_iff, mem_pointwise_smul_iff_inv_smul_mem,
    ← ConjAct.toConjAct_inv, ConjAct.toConjAct_smul, mem_normalizer_iff, inv_inv, Iff.comm]

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

Goal state before:
pp: α : Type u_6
a : Multiset α
l : List (Multiset α)
⊢ Disjoint l.sum a ↔ ∀ b ∈ l, Disjoint b a

Tactic:
induction l with
  | nil =>
    simp only [zero_disjoint, List.not_mem_nil, IsEmpty.forall_iff, forall_const, List.sum_nil]
  | cons b bs ih =>
    simp [ih]

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_4
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
f : F
h : ker f ≤ c
hf : Surjective ⇑f
⊢ mapGen ⇑f = mapOfSurjective f h hf

Tactic:
rw [← conGen_of_con (c.mapOfSurjective f h hf)]

Goal state after:
M : Type u_1
N : Type u_2
F : Type u_4
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
f : F
h : ker f ≤ c
hf : Surjective ⇑f
⊢ mapGen ⇑f = conGen ⇑(mapOfSurjective f h hf)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
p : ι → Prop
inst✝ : DecidablePred p
hp : ∀ x ∈ s, f x ≠ 1 → p x
x : ι
h₁ : x ∈ s
h₂ : ¬f x = 1
⊢ p x

Tactic:
simpa using hp _ h₁ h₂

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
⊢ (QuotientGroup.con H).subgroup = H

Tactic:
ext
  simp [QuotientGroup.con, leftRel_apply]

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
f s : ℕ → M
base : s 0 = 1
n : ℕ
step : ∀ k < n, s (k + 1) = s k * f k
⊢ ∏ k ∈ range n, f k = s n

Tactic:
by
  induction n with
  | zero => rw [Finset.prod_range_zero, base]
  | succ k hk =>
    rw [Finset.prod_range_succ, step _ (Nat.lt_succ_self _), hk]
    exact fun _ hl ↦ step _ (Nat.lt_succ_of_lt hl)

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case intro
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
inst✝ : Finite G
val✝ : Fintype G
⊢ FG G

Tactic:
exact ⟨⟨Finset.univ, by rw [Finset.coe_univ]; exact Subgroup.closure_univ⟩⟩

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

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

Tactic:
by
  conv_lhs => rw [Finset.eq_prod_range_div f]
  simp [Finset.prod_range_succ', mul_comm]

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

Goal state before:
pp: ι : Type u_1
M : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : CommMonoid M
f : ι → M
a : ι
l : List ι
hl : (a :: l).Nodup
⊢ (a :: l).toFinset.prod f = (map f (a :: l)).prod

Tactic:
by
    let ⟨notMem, hl⟩ := List.nodup_cons.mp hl
    simp [Finset.prod_insert (mt List.mem_toFinset.mp notMem), prod_toFinset _ hl]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ⁅⁅H₂, H₃⁆, H₁⁆ = ⊥
h2 : ⁅⁅H₃, H₁⁆, H₂⁆ = ⊥
⊢ ⁅⁅H₁, H₂⁆, H₃⁆ = ⊥

Tactic:
simp_rw [commutator_eq_bot_iff_le_centralizer, commutator_le,
    mem_centralizer_iff_commutator_eq_one] at h1 h2 ⊢
  intro x hx y hy z hz
  trans x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹
  -- We avoid `group` here to minimize imports while low in the hierarchy;
  -- typically it would be better to invoke the tactic.
  · simp [commutatorElement_def, mul_assoc]
  · rw [h1 _ (H₂.inv_mem hy) _ hz _ (H₁.inv_mem hx), h2 _ (H₃.inv_mem hz) _ (H₁.inv_mem hx) _ hy]
    simp [mul_assoc]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ commutator G = normalClosure (commutatorSet G)

Tactic:
by
  simp [commutator, Subgroup.commutator_def', commutatorSet]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
y x1 x2 : FreeAbelianGroup α
ih1 : x1 * y = y * x1
ih2 : x2 * y = y * x2
⊢ (x1 + x2) * y = y * (x1 + x2)

Tactic:
rw [add_mul, mul_add, ih1, ih2]

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
h₀ : x 0 ≤ y 0
hx : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
⊢ x n ≤ y n

Tactic:
induction n with
  | zero => exact h₀
  | succ n ihn =>
    refine (hx _ n.lt_succ_self).trans ((hf <| ihn ?_ ?_).trans (hy _ n.lt_succ_self))
    · exact fun k hk => hx _ (hk.trans n.lt_succ_self)
    · exact fun k hk => hy _ (hk.trans n.lt_succ_self)

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

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

Tactic:
by_cases h : IsMax a
  · rw [h.succ_eq, (f.isMax_apply.2 h).succ_eq]
  · exact ((apply_covBy_apply_iff f).2 <| covBy_succ_of_not_isMax h).succ_eq.symm

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

Goal state before:
pp: case pos
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
hm' : m ∈ S
⊢ ∃ x, IsGreatest S x

pp: case neg
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
hm' : m ∉ S
⊢ ∃ x, IsGreatest S x

Tactic:
· exact ⟨_, hm', hm⟩

Goal state after:
case neg
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
hm' : m ∉ S
⊢ ∃ x, IsGreatest S x
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x : α
inst✝³ : PartialOrder α
inst✝² : AddMonoidWithOne α
inst✝¹ : SuccAddOrder α
inst✝ : IsBotZeroClass α
hx : IsSuccLimit x
⊢ ∀ (n : ℕ), ↑n < x

Tactic:
simpa using hx.add_natCast_lt hx.pos

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

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
hα : Nonempty α
a✝ : PredOrder (WithTop α)
a : α
h : pred ⊤ = ↑a
c : α
hc : ↑a < ↑c
⊢ False

Tactic:
← h

Goal state after:
case coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
hα : Nonempty α
a✝ : PredOrder (WithTop α)
a : α
h : pred ⊤ = ↑a
c : α
hc : pred ⊤ < ↑c
⊢ False
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : ℕ∞
⊢ n < 2 ↔ n ≤ 1

Tactic:
by
  rw [← one_add_one_eq_two, lt_add_one_iff one_ne_top]

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

Goal state before:
pp: case inr.inr.coe
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
y : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
hy : y ≠ 0
x : ℕ
hx : ↑x ≠ 0
⊢ map (⇑f) (↑x * y) = map ⇑f ↑x * map (⇑f) y

Tactic:
induction y with

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

Goal state before:
pp: case nil
α : Type u_1
n i : ℕ
ih : i < n - 1
h✝ : [].length = n
h : 0 = n
⊢ (tail ⟨[], h✝⟩).get ⟨i, ih⟩ = get ⟨[], h✝⟩ ⟨i + 1, ⋯⟩

Tactic:
← h

Goal state after:
case nil
α : Type u_1
n i : ℕ
ih✝ : i < n - 1
ih : i < 0 - 1
h✝ : [].length = n
h : 0 = n
⊢ (tail ⟨[], h✝⟩).get ⟨i, ih✝⟩ = get ⟨[], h✝⟩ ⟨i + 1, ⋯⟩
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
a : List α
ha : a ∈ {x ∈ T | x.length = s}
hlen : a ∈ T ∧ a.length = s := mem_filter.mp ha
j : Fin s
⊢ ↑j < a.length

Tactic:
simp [hlen]

Goal state after:
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
a : List α
ha : a ∈ {x ∈ T | x.length = s}
hlen : a ∈ T ∧ a.length = s := mem_filter.mp ha
⊢ (List.ofFn fun j ↦ a.get ⟨↑j, ⋯⟩).length = a.length

Tactic:
simp [hlen]

Goal state after:
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∏ a ∈ {x | p x}.toFinset, f a = ∏ a, f ↑a

Tactic:
← Finset.prod_subtype

Goal state after:
α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∏ a ∈ {x | p x}.toFinset, f a = ∏ a ∈ ?s, f a

case s
α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ Finset α

case h
α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∀ (x : α), x ∈ ?s ↔ p x
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : sSup (Iio x) = x
hx : ¬IsSuccPrelimit x
⊢ False

Tactic:
← h

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : sSup (Iio x) = x
hx : ¬IsSuccPrelimit (sSup (Iio x))
⊢ False
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: ι : Type u_1
f : ι → Cardinal.{u}
⊢ prod f = 0 ↔ ∃ i, f i = 0

Tactic:
lift f to ι → Type u using fun _ => trivial
  simp only [mk_eq_zero_iff, ← mk_pi, isEmpty_pi]

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

Goal state before:
pp: case inr.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a : β
b : α
⊢ (Equiv.sumComm α β) (inr a) ≤ (Equiv.sumComm α β) (inl b) ↔ inr a ≤ inl b

Tactic:
exact iff_of_true (@Lex.inl_le_inr (OrderDual β) (OrderDual α) _ _ _ _)
          (Lex.inl_le_inr _ _)

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

Goal state before:
pp: case mpr
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ : α
⊢ ∀ (a₂ : α), (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂

Tactic:
a₂

Goal state after:
case mpr
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
⊢ (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: case zero
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁✝ a₂ a₁ : α
⊢ ∀ (a₂ : α), (⇑f)^[0] (a₁ ⊔ a₂) ≤ (⇑f)^[0] a₁ ⊔ a₂

Tactic:
a₂

Goal state after:
case zero
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁✝ a₂✝ a₁ a₂ : α
⊢ (⇑f)^[0] (a₁ ⊔ a₂) ≤ (⇑f)^[0] a₁ ⊔ a₂
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: case succ
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁✝ a₂ : α
n : ℕ
ih : ∀ (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂
a₁ : α
⊢ ∀ (a₂ : α), (⇑f)^[n + 1] (a₁ ⊔ a₂) ≤ (⇑f)^[n + 1] a₁ ⊔ a₂

Tactic:
a₂

Goal state after:
case succ
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁✝ a₂✝ : α
n : ℕ
ih : ∀ (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂
a₁ a₂ : α
⊢ (⇑f)^[n + 1] (a₁ ⊔ a₂) ≤ (⇑f)^[n + 1] a₁ ⊔ a₂
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set (α × β))
⊢ ScottContinuousOn D Prod.fst

Tactic:
by
  intro d hd₁ hd₂ hd₃ a ha
  simp only [isLUB_prod] at ha
  exact ha.1

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
x : α
⊢ some x ≠ none

Tactic:
intro h
  exact true_ne_false (congr_arg Dom h)

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ {y | IsExtremePt x f y}
⊢ ∀ {z : α}, z ∈ bot x f → z < f y → f z ≤ f y

Tactic:
intro z

Goal state after:
case image_self_subset_self
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ {y | IsExtremePt x f y}
z : α
⊢ z ∈ bot x f → z < f y → f z ≤ f y
Module: Mathlib.Order.Zorn

Goal state before:
pp: α : Type u_1
r : α → α → Prop
h : ∀ (c : Set α), IsChain r c → ∃ ub, ∀ a ∈ c, r a ub
trans : ∀ {a b c : α}, r a b → r b c → r a c
this✝ : ∃ ub, ∀ a ∈ maxChain r, r a ub
ub : α
hub : ∀ a ∈ maxChain r, r a ub
a : α
ha : r ub a
this : IsChain r (insert a (maxChain r))
⊢ a ∈ maxChain r

Tactic:
maxChain_spec.right this (subset_insert _ _)

Goal state after:
α : Type u_1
r : α → α → Prop
h : ∀ (c : Set α), IsChain r c → ∃ ub, ∀ a ∈ c, r a ub
trans : ∀ {a b c : α}, r a b → r b c → r a c
this✝ : ∃ ub, ∀ a ∈ maxChain r, r a ub
ub : α
hub : ∀ a ∈ maxChain r, r a ub
a : α
ha : r ub a
this : IsChain r (insert a (maxChain r))
⊢ a ∈ insert a (maxChain r)
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
h : ∀ z ∈ c, f z ≤ y
⊢ ∀ y_1 ∈ c.carrier, y_1 ≤ y

Tactic:
intro z

Goal state after:
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
h : ∀ z ∈ c, f z ≤ y
z : α
⊢ z ∈ c.carrier → z ≤ y
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case union
α : Type u_1
r : α → α → Prop
c : Set α
s✝ : Set (Set α)
hs : ∀ a ∈ s✝, ChainClosure r a
h : ∀ a ∈ s✝, IsChain r a
⊢ IsChain r (⋃₀ s✝)

Tactic:
| union hs h =>

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case pos
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ a, some a ∈ c
h : some (Classical.choose h_1) = some a
h' : some (Classical.choose h_1) ∈ c
⊢ some a ∈ c

Tactic:
← h

Goal state after:
case pos
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ a, some a ∈ c
h : some (Classical.choose h_1) = some a
h' : some (Classical.choose h_1) ∈ c
⊢ some (Classical.choose h_1) ∈ c
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: c : Cardinal.{u_1}
h : ↑(toNat c) = c
⊢ c < ℵ₀

Tactic:
← h

Goal state after:
c : Cardinal.{u_1}
h : ↑(toNat c) = c
⊢ ↑(toNat c) < ℵ₀
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: x : Cardinal.{u_1}
hx : x ≤ ℵ₀
⊢ x ∈ range ofENat

Tactic:
rcases hx.lt_or_eq with hlt | rfl

Goal state after:
case inl
x : Cardinal.{u_1}
hx : x ≤ ℵ₀
hlt : x < ℵ₀
⊢ x ∈ range ofENat

case inr
hx : ℵ₀ ≤ ℵ₀
⊢ ℵ₀ ∈ range ofENat
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_1
α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : β → Cardinal.{v}
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = lift.{u, v} (∏ i, f (e i))

Tactic:
← h

Goal state after:
case refine_1
α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : β → Cardinal.{v}
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = prod fun i ↦ f (e i)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: s : Set Cardinal.{v}
⊢ lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)

Tactic:
by
  rcases eq_empty_or_nonempty s with (rfl | hs)
  · simp
  · exact lift_monotone.map_csInf hs

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
hf : BddAbove (range f)
g : Cardinal.{v} → Cardinal.{max v w}
⊢ BddAbove (range (g ∘ f))

Tactic:
by
  rw [range_comp]
  exact bddAbove_image g hf

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

Goal state before:
pp: ι : Type u
inst✝ : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (range f)
n : ℕ
h : ⨆ i, f i = ↑n
⊢ ∃ i, f i = ↑n

Tactic:
← h

Goal state after:
ι : Type u
inst✝ : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (range f)
n : ℕ
h : ⨆ i, f i = ↑n
⊢ ∃ i, f i = ⨆ i, f i
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u_1
s : Set α
⊢ #↑s + #↑sᶜ = #α

Tactic:
classical
  exact mk_congr (Equiv.Set.sumCompl s)

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set β
h : f '' f ⁻¹' s = s
⊢ lift.{u, v} #↑s ≤ lift.{v, u} #↑(f ⁻¹' s)

Tactic:
← h

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set β
h : f '' f ⁻¹' s = s
⊢ lift.{u, v} #↑(f '' f ⁻¹' s) ≤ lift.{v, u} #↑(f ⁻¹' s)
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
⊢ (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)

Tactic:
induction k with
  | zero => simp [one_eq_id]
  | succ k ih => rw [pow_succ', pow_succ', mul_eq_comp, LinearMap.comp_assoc, ih,
    ← LinearMap.comp_assoc, h, LinearMap.comp_assoc, mul_eq_comp]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R' : Type u_4
M' : Type u_5
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
S T : Submodule R' M'
s t : M'
hs : s ∈ S
ht : t ∈ T
⊢ s - t ∈ S ⊔ T

Tactic:
by
  rw [sub_eq_add_neg]
  exact add_mem_sup hs (neg_mem ht)

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Ker

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : ∀ x ∈ p, f x ∈ q
⊢ (codRestrict q (f.domRestrict p) ⋯).ker = comap p.subtype f.ker

Tactic:
ker_codRestrict,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : ∀ x ∈ p, f x ∈ q
⊢ (f.domRestrict p).ker = comap p.subtype f.ker
Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : Type u_9
n : Type u_10
p : Type u_11
e : m ≃ n
x : m → M
i : m
⊢ (funLeft R M ⇑e ∘ₗ funLeft R M ⇑e.symm) x i = x i

Tactic:
← funLeft_comp,

Goal state after:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : Type u_9
n : Type u_10
p : Type u_11
e : m ≃ n
x : m → M
i : m
⊢ (funLeft R M (⇑e.symm ∘ ⇑e)) x i = x i