mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α✝ : Type u
L L₁ L₂ L₃ L₄ : List (α✝ × Bool)
β✝ : Type v
f : α✝ → β✝
x✝ y : FreeGroup α✝
α : Type ?u.38
β : Type ?u.39
e : α ≃ β
x : FreeGroup α
⊢ (map ⇑e.symm) ((map ⇑e) x) = x

Tactic:
simp [map.comp]

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

Goal state before:
pp: α✝ : Type u
L L₁ L₂ L₃ L₄ : List (α✝ × Bool)
β✝ : Type v
f : α✝ → β✝
x✝ y : FreeGroup α✝
α : Type ?u.38
β : Type ?u.39
e : α ≃ β
x : FreeGroup β
⊢ (map ⇑e) ((map ⇑e.symm) x) = x

Tactic:
simp [map.comp]

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ Function.LeftInverse (fun x ↦ of () ^ x) fun x ↦ ((map fun x ↦ 1) x).sum

Tactic:
rintro ⟨L⟩
    simp only [quot_mk_eq_mk, map.mk, sum_mk, List.map_map]
    exact List.recOn L
     rfl
     (fun ⟨⟨⟩, b⟩ tl ih => by
        cases b <;> simp [zpow_add, ih] <;> rfl)

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
l : List ι
f : ι → M
⊢ (List.map f l).prod = ∏ m ∈ l.toFinset, f m ^ count m l

Tactic:
induction l with

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
i : κ
⊢ i ∈ ↑s → ∀ ⦃y : κ⦄, y ∈ ↑s → i ≠ y → (_root_.Disjoint on t') i y

Tactic:
hi

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
i : κ
hi : i ∈ ↑s
⊢ ∀ ⦃y : κ⦄, y ∈ ↑s → i ≠ y → (_root_.Disjoint on t') i y
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : PartialOrder M
inst✝⁴ : Sub M
inst✝³ : OrderedSub M
inst✝² : AddLeftMono M
inst✝¹ : AddLeftReflectLE M
inst✝ : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n : ℕ
⊢ f 0 - f 0 = 0

Tactic:
apply tsub_eq_of_eq_add; rw [zero_add]

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

Goal state before:
pp: case hx
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ map f ⊤ = f.range

Tactic:
rw [Subgroup.map_eq_range_iff]
    rw [codisjoint_iff, top_sup_eq]

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

Goal state before:
pp: case hy
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ map f ⊤ = f.range

Tactic:
rw [Subgroup.map_eq_range_iff]
    rw [codisjoint_iff, top_sup_eq]

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : N
⊢ f ((f.sec (x * y)).1 * ↑(f.sec y).2 * ↑(f.sec x).2) = f ((f.sec y).1 * ↑(f.sec (x * y)).2 * (f.sec x).1)

Tactic:
simp_rw [map_mul, sec_spec', ← toMonoidHom_apply]

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : N
⊢ f.toMonoidHom ↑(f.sec (x * y)).2 * (x * y) * f.toMonoidHom ↑(f.sec y).2 * f.toMonoidHom ↑(f.sec x).2 =
    f.toMonoidHom ↑(f.sec y).2 * y * f.toMonoidHom ↑(f.sec (x * y)).2 * (f.toMonoidHom ↑(f.sec x).2 * x)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (r S) x y ↔ ∃ c, ↑c * (↑y.2 * x.1) = ↑c * (↑x.2 * y.1)

Tactic:
simp only [r_eq_r' S, r', Con.rel_mk]

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

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (∃ a ∈ S, a * (↑y.2 * x.1) = a * (↑x.2 * y.1)) → ∃ a ∈ S, ∃ v, a * y.1 = v * x.1 ∧ a * ↑y.2 = v * ↑x.2

Tactic:
rintro ⟨u, hu, e⟩
    exact ⟨_, mul_mem hu x.2.2, u * y.2, by rw [mul_assoc, mul_assoc, ← e], mul_right_comm _ _ _⟩

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

Goal state before:
pp: M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
⊢ (k.map hl j).comp (f.map hy k) = f.map ⋯ j

Tactic:
ext z

Goal state after:
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
z : N
⊢ ((k.map hl j).comp (f.map hy k)) z = (f.map ⋯ j) z
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ ↑sc * ↑sa * r₁ = ↑sc * (ra * ↑s₂)

Tactic:
← ha,

Goal state after:
case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ ↑sc * ↑sa * r₁ = ↑sc * (↑sa * r₁)
Module: Mathlib.Algebra.Ring.Equiv

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
hf : Function.Bijective ⇑f
⊢ (↑(ofBijective f hf).symm).comp f = NonUnitalRingHom.id R

Tactic:
by
  ext
  exact (RingEquiv.ofBijective f hf).injective <| RingEquiv.apply_symm_apply ..

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

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : α
h₀ : 0 < ↑a
c : WithTop α
b : α
hbc : ↑b < c
⊢ (fun x ↦ ↑a * x) ↑b < (fun x ↦ ↑a * x) c

Tactic:
match c with
  | ⊤ => simp [← coe_mul, mul_top h₀.ne']
  | (c : α) =>
  simp only [coe_pos, coe_lt_coe, ← coe_mul, gt_iff_lt] at *
  exact mul_lt_mul_of_pos_left hbc h₀

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

Goal state before:
pp: R : Type u_1
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
r : R
x : OreLocalization S X
⊢ (r • 1 /ₒ 1) • x = r • x

Tactic:
by
  rw [oreDiv_one_smul, smul_one_smul]

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

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
⊢ x ^ n = ⊤ ↔ x = ⊤ ∧ n ≠ 0

Tactic:
cases x <;> cases n <;> simp [← coe_pow]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
⊢ ∀ (a b : SuccOrder α), a = b

Tactic:
intro h₀

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
h₀ : SuccOrder α
⊢ ∀ (b : SuccOrder α), h₀ = b
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝⁴ : PartialOrder α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
⊢ x ⋖ y ↔ x + 1 = y

Tactic:
by
  rw [← succ_eq_add_one]
  exact succ_eq_iff_covBy.symm

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

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
h : x - 1 < y
⊢ x ≤ y

Tactic:
rw [← pred_eq_sub_one] at h

Goal state after:
α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
h : pred x < y
⊢ x ≤ y
Module: Mathlib.Data.ENat.Basic

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

Tactic:
lt_add_one_iff one_ne_top

Goal state after:
n : ℕ∞
⊢ n ≤ 1 ↔ n ≤ 1
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case neg.inl
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h' : pred x ∉ s
h✝¹ : ⟨x, hx⟩ ≤ ⟨x, hx⟩
y : α
hy : y ∈ s
h✝ : ⟨y, hy⟩ ≤ ⟨x, hx⟩
h : ⟨y, hy⟩ < ⟨x, hx⟩
⊢ ⟨x, hx⟩ ≤ ⟨y, hy⟩

pp: case neg.inr
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h' : pred x ∉ s
h✝¹ : ⟨x, hx⟩ ≤ ⟨x, hx⟩
y : α
hy : y ∈ s
h✝ : ⟨y, hy⟩ ≤ ⟨x, hx⟩
h : ⟨y, hy⟩ = ⟨x, hx⟩
⊢ ⟨x, hx⟩ ≤ ⟨y, hy⟩

Tactic:
· simp only [Subtype.mk_lt_mk] at h
        have := h.le_pred
        absurd h'
        apply out' hy hx
        simp [this, Order.pred_le]

Goal state after:
case neg.inr
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h' : pred x ∉ s
h✝¹ : ⟨x, hx⟩ ≤ ⟨x, hx⟩
y : α
hy : y ∈ s
h✝ : ⟨y, hy⟩ ≤ ⟨x, hx⟩
h : ⟨y, hy⟩ = ⟨x, hx⟩
⊢ ⟨x, hx⟩ ≤ ⟨y, hy⟩
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) < f a
⊢ StrictMono f

Tactic:
by
  simpa using strictMonoOn_of_pred_lt Set.ordConnected_univ (by simpa using hf)

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

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
hs : i ∉ s
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

Tactic:
simp_all only [not_false_eq_true, forall_const, one_mul]
    apply Finset.prod_congr <;> aesop

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

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : β
⊢ i ∈ (image b univ).erase k → i ∈ image (fun i ↦ b ↑i) univ

Tactic:
hi

Goal state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ (image b univ).erase k
⊢ i ∈ image (fun i ↦ b ↑i) univ
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ image (fun i ↦ b ↑i) univ = (image b univ).erase k

Tactic:
apply subset_antisymm
  · rw [image_subset_iff]
    intro i _
    apply mem_erase_of_ne_of_mem i.2 (mem_image_of_mem _ (mem_univ _))
  · intro i hi
    rw [mem_image]
    rcases mem_image.1 (erase_subset _ _ hi) with ⟨a, _, ha⟩
    subst ha
    exact ⟨⟨a, ne_of_mem_erase hi⟩, mem_univ _, rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_6
f : β → α → β
b : β
m✝ : Fin (0 + 1)
⊢ (scanl f b nil).get m✝ = (b ::ᵥ nil).get m✝

Tactic:
simp [scanl, get]

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Encodable α✝
α : Type u_2
inst✝ : Countable α
⊢ Countable (List α)

Tactic:
by
  have := Encodable.ofCountable α
  infer_instance

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
⊢ ∃ f, s = range f

Tactic:
rcases hc.exists_surjective hs with ⟨f, hf⟩

Goal state after:
α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
f : ℕ → ↑s
hf : Surjective f
⊢ ∃ f, s = range f
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
⊢ Countable ↑{t | (f t).Nonempty}

Tactic:
have A : Injective F := by
    rintro ⟨t, ht⟩ ⟨t', ht'⟩ htt'
    have A : (f t ∩ f t').Nonempty := by
      refine ⟨F ⟨t, ht⟩, hF ⟨t, _⟩, ?_⟩
      rw [htt']
      exact hF ⟨t', _⟩
    simp only [Subtype.mk.injEq]
    by_contra H
    exact not_disjoint_iff_nonempty_inter.2 A (hf H)

Goal state after:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
A : Injective F
⊢ Countable ↑{t | (f t).Nonempty}
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ a ∈ o.toOption ↔ a ∈ o

Tactic:
by
  unfold toOption
  by_cases h : o.Dom
  · simpa [h] using ⟨fun h => ⟨_, h⟩, fun ⟨_, h⟩ => h⟩
  · simp only [h, ↓reduceDIte, Option.mem_def, reduceCtorEq, false_iff]
    exact mt Exists.fst h

Goal state after:
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case succ
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s✝ : Set α
hc₁ : ChainClosure r s✝
h : s✝ ⊆ c₂
⊢ SuccChain r s✝ ⊆ c₂

Tactic:
| succ hc₁ h =>

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
c : Chain (Part α)
a : α
h : a ∈ Part.ωSup c
⊢ some a ∈ c

Tactic:
simp only [Part.ωSup] at h; split_ifs at h with h_1
  · have h' := Classical.choose_spec h_1
    rw [← eq_some_iff] at h
    rw [← h]
    exact h'
  · rcases h with ⟨⟨⟩⟩

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
x : α
c : Chain (Part α)
⊢ x ∈ ωSup c ↔ some x ∈ c

Tactic:
simp only [ωSup, Part.ωSup]
  constructor
  · exact fun a ↦ mem_chain_of_mem_ωSup a
  · intro h
    have h' : ∃ a : α, some a ∈ c := ⟨_, h⟩
    rw [dif_pos h']
    have hh := Classical.choose_spec h'
    rw [eq_of_chain hh h]
    simp

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

Goal state before:
pp: case inl
b : Cardinal.{u_1}
hb : 1 ≤ b
⊢ 0 ≤ 0 ^ b

pp: case inr
a b : Cardinal.{u_1}
hb : 1 ≤ b
ha : a ≠ 0
⊢ a ≤ a ^ b

Tactic:
· exact zero_le

Goal state after:
case inr
a b : Cardinal.{u_1}
hb : 1 ≤ b
ha : a ≠ 0
⊢ a ≤ a ^ b
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ⇑F
sG : Surjective G
i : ι
⊢ ∃ b, ∀ (a : Quotient.out (f i)), G ⟨i, a⟩ i ≠ b

Tactic:
simp only [not_exists.symm, not_forall.symm]

Goal state after:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ⇑F
sG : Surjective G
i : ι
⊢ ¬∀ (x : Quotient.out (g i)), ∃ x_1, G ⟨i, x_1⟩ i = x
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: n : ℕ
a : Cardinal.{u}
⊢ ↑n = lift.{v, u} a ↔ ↑n = a

Tactic:
← lift_natCast.{v, u} n,

Goal state after:
n : ℕ
a : Cardinal.{u}
⊢ lift.{v, u} ↑n = lift.{v, u} a ↔ ↑n = a
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: ⊢ range ofENat = Iic ℵ₀

Tactic:
refine (range_subset_iff.2 ofENat_le_aleph0).antisymm fun x (hx : x ≤ ℵ₀) ↦ ?_
  rcases hx.lt_or_eq with hlt | rfl
  · lift x to ℕ using hlt
    exact mem_range_self (x : ℕ∞)
  · exact mem_range_self (⊤ : ℕ∞)

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
a b : R
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ↔ IsSMulRegular M a ∧ IsSMulRegular M b

Tactic:
rw [← mul_and_mul_iff]

Goal state after:
R : Type u_1
M : Type u_3
a b : R
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ↔ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: n : ℕ
⊢ succ ↑n = ↑n + 1

Tactic:
refine (succ_le_of_lt ?_).antisymm (add_one_le_of_lt <| lt_succ _)
  rw [← Nat.cast_succ]
  exact Nat.cast_lt.2 (Nat.lt_succ_self _)

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic

Goal state before:
pp: M : Type u_1
β : Type u_2
α : Type u_3
N : Type u_4
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
x y : β
hne : mk.symm c₁ • a ≠ mk.symm c₂ • a
this : DecidableEq α
⊢ x = y

Tactic:
replace h := congr_fun (h (update (const α x) (mk.symm c₂ • a) y)) a

Goal state after:
M : Type u_1
β : Type u_2
α : Type u_3
N : Type u_4
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
a : α
x y : β
hne : mk.symm c₁ • a ≠ mk.symm c₂ • a
this : DecidableEq α
h : (c₁ • update (const α x) (mk.symm c₂ • a) y) a = (c₂ • update (const α x) (mk.symm c₂ • a) y) a
⊢ x = y
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst✝⁸ : Semiring R₁
inst✝⁷ : Semiring R₂
inst✝⁶ : Semiring R₃
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
σ₃₂ : R₃ →+* R₂
inst✝¹ : RingHomInvPair σ₂₃ σ₃₂
inst✝ : RingHomCompTriple σ₁₃ σ₃₂ σ₁₂
h : M₁ →ₛₗ[σ₁₃] M₃
f' : M₃ →ₛₗ[σ₃₂] M₂
hf' : f ∘ₛₗ f' = id
⊢ (fun g ↦ f ∘ₛₗ g) (f' ∘ₛₗ h) = h

Tactic:
simp_rw [← comp_assoc, hf', id_comp]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
h : Surjective ⇑f'
n : ℕ
⊢ Surjective ⇑(f' ^ (n + 1))

Tactic:
iterate_succ

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
h : Surjective ⇑f'
n : ℕ
⊢ Surjective ⇑((f' ^ n) ∘ₗ f')
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
h : Injective ⇑f'
n : ℕ
⊢ Injective ⇑(f' ^ (n + 1))

Tactic:
iterate_succ

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
h : Injective ⇑f'
n : ℕ
⊢ Injective ⇑((f' ^ n) ∘ₗ f')
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
h : Bijective ⇑f'
n : ℕ
⊢ Bijective ⇑(f' ^ (n + 1))

Tactic:
iterate_succ

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
h : Bijective ⇑f'
n : ℕ
⊢ Bijective ⇑((f' ^ n) ∘ₗ f')
Module: Mathlib.Algebra.Ring.Prod

Goal state before:
pp: R : Type u_1
S : Type u_3
T : Type u_5
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
f : R →ₙ+* S × T
x : R
⊢ (((fst S T).comp f).prod ((snd S T).comp f)) x = f x

Tactic:
simp only [prod_apply, coe_fst, coe_snd, comp_apply]

Goal state after:
Module: Mathlib.Algebra.Ring.Prod

Goal state before:
pp: R : Type u_1
S : Type u_3
T : Type u_5
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
f : R →+* S × T
x : R
⊢ (((fst S T).comp f).prod ((snd S T).comp f)) x = f x

Tactic:
simp only [prod_apply, coe_fst, coe_snd, comp_apply]

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
h : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x ∈ closure s

Tactic:
by
    induction h using AddSubgroup.closure_induction with
    | mem _ hx => induction hx using Subsemigroup.closure_induction with
      | mem _ h => exact subset_closure h
      | mul _ _ _ _ h₁ h₂ => exact mul_mem h₁ h₂
    | zero => exact zero_mem _
    | add _ _ _ _ h₁ h₂ => exact add_mem h₁ h₂
    | neg _ _ h => exact neg_mem h

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case refine_2
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y * ↑u = A * B
⊢ IsUnit A ∨ IsUnit B

Tactic:
rw [← u⁻¹.isUnit_mul_units B]
    apply h
    rw [← mul_assoc, ← HAB, Units.mul_inv_cancel_right]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_2
N : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
x y : M
u : Mˣ
ha : x * ↑u = y
⊢ f x * ↑((Units.map ↑f) u) = f y

Tactic:
← ha,

Goal state after:
M : Type u_2
N : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
x y : M
u : Mˣ
ha : x * ↑u = y
⊢ f x * ↑((Units.map ↑f) u) = f (x * ↑u)
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b c d : M
⊢ a * b ~ᵤ c * d → b ~ᵤ d → b ≠ 0 → a ~ᵤ c

Tactic:
rw [mul_comm a, mul_comm c]; exact Associated.of_mul_left

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

Goal state before:
pp: R : Type u_10
R₂ : Type u_11
M : Type u_12
M₂ : Type u_13
inst✝⁶ : Semiring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ (-f).range = f.range

Tactic:
change range ((-LinearMap.id : M₂ →ₗ[R₂] M₂).comp f) = _

Goal state after:
R : Type u_10
R₂ : Type u_11
M : Type u_12
M₂ : Type u_13
inst✝⁶ : Semiring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ ((-id) ∘ₛₗ f).range = f.range
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: case mp
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
N : Submodule R M
x✝ : M
hx : x✝ ∈ sInf {p | ∀ ⦃r : S⦄ {n : M}, r ∈ ∅ → n ∈ N → r • n ∈ p}
⊢ x✝ ∈ ⊥

Tactic:
Submodule.mem_sInf

Goal state after:
case mp
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
N : Submodule R M
x✝ : M
hx : ∀ p ∈ {p | ∀ ⦃r : S⦄ {n : M}, r ∈ ∅ → n ∈ N → r • n ∈ p}, x✝ ∈ p
⊢ x✝ ∈ ⊥
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: case le
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r : S
m : M
hm : m ∈ ↑N
⊢ (DistribSMul.toLinearMap R M r) m ∈ sInf {p | ∀ ⦃r_1 : S⦄ {n : M}, r_1 ∈ {r} → n ∈ N → r_1 • n ∈ p}

Tactic:
Submodule.mem_sInf

Goal state after:
case le
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r : S
m : M
hm : m ∈ ↑N
⊢ ∀ p ∈ {p | ∀ ⦃r_1 : S⦄ {n : M}, r_1 ∈ {r} → n ∈ N → r_1 • n ∈ p}, (DistribSMul.toLinearMap R M r) m ∈ p