mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ x✝¹ * x✝ * ↑(Int.negSucc n) = x✝¹ * (x✝ * ↑(Int.negSucc n))

Tactic:
simp only [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev]
        rw [mul_add, mul_add, mul_add, mul_neg, mul_one, mul_neg, mul_neg, mul_one, mul_neg,
          add_right_inj, (natCast_mem_center _ n).right_assoc _ _, mul_neg, mul_neg]

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

Goal state before:
pp: M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝ : M
⊢ -a * x✝ = a * -x✝

Tactic:
neg_mul_comm

Goal state after:
M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝ : M
⊢ a * -x✝ = a * -x✝
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: case mp.right
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
h : u ≤ s.prod t
⊢ map (snd M N) u ≤ t

Tactic:
· rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
      exact (h hy1).2

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝² : G
x✝¹ x✝ : R
⊢ (algebraMap R A) (x✝² • (x✝¹ + x✝)) = (algebraMap R A) (x✝² • x✝¹ + x✝² • x✝)

Tactic:
rw [algebraMap.smul', map_add, smul_add, ← algebraMap.smul', ← algebraMap.smul', ← map_add]

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:
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 : ↑u * y = A * B
⊢ IsUnit A ∨ IsUnit B

Tactic:
← u⁻¹.isUnit_units_mul

Goal state after:
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 : ↑u * y = A * B
⊢ IsUnit (↑u⁻¹ * A) ∨ IsUnit B
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
⊢ nonZeroDivisorsRight M₀ = nonZeroDivisorsLeft M₀

Tactic:
by
  rw [nonZeroDivisorsLeft_eq_right]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b c d : Associates M
h₁ : a ≤ b
h₂ : c ≤ d
x : Associates M
hx : b = a * x
y : Associates M
hy : d = c * y
⊢ b * d = a * c * (x * y)

Tactic:
simp [hx, hy, mul_comm, mul_left_comm]

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

Goal state before:
pp: case hs
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f g : M →ₛₗ[τ₁₂] M₂
w✝ : M
⊢ f w✝ ∈ f.range

Tactic:
simp only [mem_range, exists_apply_eq_apply]

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

Goal state before:
pp: case ht
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f g : M →ₛₗ[τ₁₂] M₂
w✝ : M
⊢ g w✝ ∈ g.range

Tactic:
simp only [mem_range, exists_apply_eq_apply]

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective ⇑i
hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ i.range
e : ↥i.range ≃ₗ[R] M₃ := (LinearEquiv.ofInjective i hi).symm
⊢ ∀ (m : R) (x : M₁), ↑e ∘ₗ codRestrict i.range (f (m • x)) ⋯ = (RingHom.id R) m • ↑e ∘ₗ codRestrict i.range (f x) ⋯

Tactic:
intro t x

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective ⇑i
hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ i.range
e : ↥i.range ≃ₗ[R] M₃ := (LinearEquiv.ofInjective i hi).symm
t : R
x : M₁
⊢ ↑e ∘ₗ codRestrict i.range (f (t • x)) ⋯ = (RingHom.id R) t • ↑e ∘ₗ codRestrict i.range (f x) ⋯
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_2.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊤ ∈ lowerBounds s
⊢ ⊤ ≤ if ⊥ ∈ s then ⊥ else ⊤

Tactic:
· rw [if_neg]
          intro con
          exact top_ne_bot (eq_bot_iff.2 (h con))

Goal state after:
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : β
⊢ ⇑e ⁻¹' Icc a b = Icc (e.symm a) (e.symm b)

Tactic:
simp [← Ici_inter_Iic]

Goal state after:
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ ⇑e.symm ⁻¹' Ioo a b = Ioo (e a) (e b)

Tactic:
e.symm.preimage_Ioo,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ Ioo (e.symm.symm a) (e.symm.symm b) = Ioo (e a) (e b)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
this : ⨆ i ∈ Finset.univ, f i = f 0 ⊔ f 1 ⊔ f 2
⊢ ⨆ i, f i = f 0 ⊔ f 1 ⊔ f 2

Tactic:
by simp [← this]

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

Goal state before:
pp: case inl
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ∅.sup id
⊢ sSup s ∈ s

Tactic:
Finset.sup_empty

Goal state after:
case inl
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ⊥
⊢ sSup s ∈ s
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
⊢ ↑t ∪ {x} ⊆ s

Tactic:
by simp [ht₁, hx₀, -Set.union_singleton]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.List

Goal state before:
pp: M₀ : Type u_4
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
a : M₀
l : List M₀
⊢ a = 0 ∨ 0 ∈ l ↔ 0 ∈ a :: l

Tactic:
mem_cons,

Goal state after:
M₀ : Type u_4
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
a : M₀
l : List M₀
⊢ a = 0 ∨ 0 ∈ l ↔ 0 = a ∨ 0 ∈ l
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
x : κ a
a✝² : x ∈ t a
y : κ a
a✝¹ : y ∈ t a
h : x ≠ y
a✝ : (a' : ι) → a' ∈ insert a s → κ a'
p₂ : (a : ι) → a ∈ s → κ a
left✝¹ : p₂ ∈ s.pi t
eq₂ : Pi.cons s a x p₂ = a✝
b✝ : (a' : ι) → a' ∈ insert a s → κ a'
p₃ : (a : ι) → a ∈ s → κ a
left✝ : p₃ ∈ s.pi t
eq₃ : Pi.cons s a y p₃ = b✝
eq : a✝ = b✝
⊢ False

Tactic:
have : Pi.cons s a x p₂ a (mem_insert_self _ _)
              = Pi.cons s a y p₃ a (mem_insert_self _ _) := by rw [eq₂, eq₃, eq]

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
x : κ a
a✝² : x ∈ t a
y : κ a
a✝¹ : y ∈ t a
h : x ≠ y
a✝ : (a' : ι) → a' ∈ insert a s → κ a'
p₂ : (a : ι) → a ∈ s → κ a
left✝¹ : p₂ ∈ s.pi t
eq₂ : Pi.cons s a x p₂ = a✝
b✝ : (a' : ι) → a' ∈ insert a s → κ a'
p₃ : (a : ι) → a ∈ s → κ a
left✝ : p₃ ∈ s.pi t
eq₃ : Pi.cons s a y p₃ = b✝
eq : a✝ = b✝
this : Pi.cons s a x p₂ a ⋯ = Pi.cons s a y p₃ a ⋯
⊢ False
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: case insert
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y → Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))
b : κ a
x✝ : b ∈ t a
h₂ : ∀ p₁ ∈ s.pi t, ∀ p₂ ∈ s.pi t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
⊢ f a b * ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯) =
    ∑ i ∈ image (Pi.cons s a b) (s.pi t), ∏ x ∈ (insert a s).attach, f (↑x) (i ↑x ⋯)

Tactic:
sum_image h₂,

Goal state after:
case insert
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y → Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))
b : κ a
x✝ : b ∈ t a
h₂ : ∀ p₁ ∈ s.pi t, ∀ p₂ ∈ s.pi t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
⊢ f a b * ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯) =
    ∑ x ∈ s.pi t, ∏ x_1 ∈ (insert a s).attach, f (↑x_1) (Pi.cons s a b x ↑x_1 ⋯)
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p q : Submodule R M
hpq : Disjoint p q
hker : f.ker ≤ q
⊢ p ⊓ q ≤ f.ker

Tactic:
hpq.eq_bot

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p q : Submodule R M
hpq : Disjoint p q
hker : f.ker ≤ q
⊢ ⊥ ≤ f.ker
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
a : α
m : M
⊢ embDomain f (single a m) = single (f a) m

Tactic:
ext b
    by_cases h : b ∈ Set.range f <;> grind

Goal state after:
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : Option α →₀ M
⊢ optionElim (f none) f.some = f

Tactic:
ext a
  cases a
  · rw [optionElim_apply_none]
  · simp

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s t : Set ι
x✝ : ι
⊢ (s ∩ t).indicator 1 x✝ = (s.indicator 1 * t.indicator 1) x✝

Tactic:
simp only [← inter_indicator_mul, Pi.mul_apply, Pi.one_apply, one_mul]

Goal state after:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s t : Set ι
x✝ : ι
⊢ (s ∩ t).indicator 1 x✝ = (s ∩ t).indicator (fun j ↦ 1) x✝
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
this : ∀ {f1 f2 : α →₀ M}, Disjoint f1.support f2.support → ∏ x ∈ f1.support, g x (f1 x + f2 x) = f1.prod g
⊢ (f1 + f2).prod g = f1.prod g * f2.prod g

Tactic:
simp_rw [← this hd, ← this hd.symm, add_comm (f2 _), Finsupp.prod, support_add_eq hd,
      prod_union hd, add_apply]

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
inst✝² : Semiring R
S : Type u_6
inst✝¹ : Semiring S
inst✝ : PartialOrder S
v : AbsoluteValue R S
⊢ ¬v.IsNontrivial ↔ ∀ (x : R), x ≠ 0 → v x = 1

Tactic:
simp only [IsNontrivial]
  push Not
  rfl

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Goal state before:
pp: case ha
α : Type u_1
β : Type u_2
inst✝³ : CommMonoidWithZero β
inst✝² : PartialOrder β
inst✝¹ : PosMulMono β
inst✝ : ZeroLEOneClass β
f : α → β
h1 : ∀ (a : α), 1 ≤ f a
a : α
s' : Multiset α
ha : a ∈ a ::ₘ s'
⊢ 0 ≤ f a

pp: case hbc
α : Type u_1
β : Type u_2
inst✝³ : CommMonoidWithZero β
inst✝² : PartialOrder β
inst✝¹ : PosMulMono β
inst✝ : ZeroLEOneClass β
f : α → β
h1 : ∀ (a : α), 1 ≤ f a
a : α
s' : Multiset α
ha : a ∈ a ::ₘ s'
⊢ 1 ≤ (map f s').prod

Tactic:
· exact le_trans (zero_le_one' β) (h1 a)

Goal state after:
case hbc
α : Type u_1
β : Type u_2
inst✝³ : CommMonoidWithZero β
inst✝² : PartialOrder β
inst✝¹ : PosMulMono β
inst✝ : ZeroLEOneClass β
f : α → β
h1 : ∀ (a : α), 1 ≤ f a
a : α
s' : Multiset α
ha : a ∈ a ::ₘ s'
⊢ 1 ≤ (map f s').prod
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s).PairwiseDisjoint f
⊢ #({i ∈ s | f i ≠ ∅}.biUnion f) + #({i ∈ s | f i = ∅}) ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})

Tactic:
filter_subset

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s).PairwiseDisjoint f
⊢ #(s.biUnion f) + #({i ∈ s | f i = ∅}) ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})
Module: Mathlib.Data.Finsupp.SMulWithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
a : R
⊢ a • 0 = 0

Tactic:
ext
    apply smul_zero

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

Goal state before:
pp: n : ℕ
s t : Finset ℕ
hs : ∀ m ∈ s, m < n
ht : ∀ m ∈ t, m < n
⊢ s.attachFin hs ⊂ t.attachFin ht ↔ s ⊂ t

Tactic:
by
  simp [← map_ssubset_map (f := Fin.valEmbedding)]

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ natAdd m '' Ioi i = Ioi (natAdd m i)

Tactic:
by
  rw [← preimage_natAdd_Ioi_natAdd, image_preimage_eq_of_subset]
  exact Ioi_subset_Ici_self.trans <| image_natAdd_Ici m i ▸ image_subset_range _ _

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
n : ℕ
⊢ (∃ x, (∀ (i : Fin n), (x i).2 ∈ s) ∧ ∑ i, (x i).1 • (x i).2 = m) → ∃ f g, ∑ i, f i • ↑(g i) = m

Tactic:
rintro ⟨f, hf, rfl⟩
    exact ⟨fun i ↦ (f i).1, fun i ↦ ⟨(f i).2, (hf i)⟩, rfl⟩

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
⊢ finSuccEquivLast (Fin.last n) = none

Tactic:
simp [finSuccEquivLast]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
⊢ f a * ∏ i ∈ Finite.toFinset hf \ {a}, f i = ∏ i ∈ Finite.toFinset hf, f i

Tactic:
Finset.sdiff_singleton_eq_erase

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
⊢ f a * ∏ i ∈ (Finite.toFinset hf).erase a, f i = ∏ i ∈ Finite.toFinset hf, f i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
hU : (mulSupport fun a ↦ ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset
⊢ ∏ᶠ (a : α), ∏ b ∈ s, f a b = ∏ b ∈ s, ∏ᶠ (a : α), f a b

Tactic:
finprod_eq_prod_of_mulSupport_subset _ hU,

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
hU : (mulSupport fun a ↦ ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset
⊢ ∏ i ∈ ⋯.toFinset, ∏ b ∈ s, f i b = ∏ b ∈ s, ∏ᶠ (a : α), f a b
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.coe.top
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
⊢ ⊤ = x ^ ↑a✝ * ⊤

Tactic:
mul_top

Goal state after:
case inr.inr.coe.top
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
⊢ ⊤ = ⊤

case inr.inr.coe.top
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
⊢ x ^ ↑a✝ ≠ 0
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCancelCommMonoid M
a b p : M
⊢ a + b ≡ b [PMOD p] ↔ a ≡ 0 [PMOD p]

Tactic:
by simp [add_comm a]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ι → ι'
g : ι' → M
hs : LinearIndepOn R (g ∘ f) s
⊢ LinearIndepOn R g (f '' s)

Tactic:
nontriviality R
  have : InjOn f s := injOn_iff_injective.2 hs.injective.of_comp
  exact (linearIndependent_equiv' (Equiv.Set.imageOfInjOn f s this) rfl).1 hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
⊢ Bijective f ↔ Injective f ∧ Nat.card α = Nat.card β

Tactic:
rw [Bijective, and_congr_right_iff]
  intro h
  have := Fintype.ofFinite β
  have := Fintype.ofInjective f h
  revert h
  rw [← and_congr_right_iff, ← Bijective,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_injective_and_card]

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ gcdB 0 s = 1

Tactic:
unfold gcdB
  rw [xgcd, xgcd_zero_left]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M M₁ : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] M₁
h : Surjective ⇑f
⊢ Module.rank R ↥f.range ≤ Module.rank R M

Tactic:
apply rank_range_le

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

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
refine ⟨x, y, z, ?_, ?_, hne, ?_⟩

Goal state after:
case refine_1.refine_1
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ x ≠ y

case refine_1.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ x ≠ z

case refine_1.refine_3
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ s = {x, y, z}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case top
α : Type u_1
s : Set α
a✝ : ∀ (n : ℕ), ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
hk : ⊤ ≤ s.encard
⊢ ∃ t ⊆ s, t.encard = ⊤

Tactic:
top_le_iff

Goal state after:
case top
α : Type u_1
s : Set α
a✝ : ∀ (n : ℕ), ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
hk : s.encard = ⊤
⊢ ∃ t ⊆ s, t.encard = ⊤
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : ⊤ ≤ k
hkt : k ≤ t.encard
hs : s.encard = ⊤
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k

Tactic:
top_le_iff

Goal state after:
case inl
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : k = ⊤
hkt : k ≤ t.encard
hs : s.encard = ⊤
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
h : (f '' s).encard = s.encard
⊢ InjOn f s

Tactic:
by
  obtain (h' | hne) := isEmpty_or_nonempty α
  · simp
  rw [← (f.invFunOn_injOn_image s).encard_image] at h
  rw [injOn_iff_invFunOn_image_image_eq_self]
  exact hs.eq_of_subset_of_encard_le' (f.invFunOn_image_image_subset s) h.symm.le

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → MulOneClass (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
⊢ (pi univ fun i ↦ closure (s i)) ≤ closure (univ.pi fun i ↦ s i)

Tactic:
by
      classical
      exact pi_le_iff.mpr fun i => map_le_of_le_comap _ <| closure_le.2 fun _x hx =>
          subset_closure <| mem_univ_pi.mpr fun j => by
        by_cases H : j = i
        · subst H
          simpa
        · simpa [H] using hs _

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ x • ↑s = y • ↑s ↔ x⁻¹ * y ∈ s

Tactic:
rw [Set.ext_iff]
  simp_rw [mem_leftCoset_iff, SetLike.mem_coe]
  constructor
  · intro h
    apply (h y).mpr
    rw [inv_mul_cancel]
    exact s.one_mem
  · intro h z
    rw [← mul_inv_cancel_right x⁻¹ y]
    rw [mul_assoc]
    exact s.mul_mem_cancel_left h

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
M✝ : Type u_5
M' : Type u_6
M : Type u_7
R : Type u_8
inst✝⁴ : Ring R
inst✝³ : Nontrivial R
inst✝² : IsAddTorsionFree R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : AddSubgroup M
ι : Type u_9
b : Basis ι R M
h : A = AddSubgroup.closure (range ⇑b)
⊢ span ℤ (range ⇑b) = AddSubgroup.toIntSubmodule A

Tactic:
by rw [h, ← Submodule.span_int_eq_addSubgroupClosure, toAddSubgroup_toIntSubmodule]

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ φ.ker
a b : G
h : φ.rangeRestrict a = φ.rangeRestrict b
⊢ φ.rangeRestrict (a⁻¹ * b) = 1

Tactic:
φ.rangeRestrict.map_mul,

Goal state after:
G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ φ.ker
a b : G
h : φ.rangeRestrict a = φ.rangeRestrict b
⊢ φ.rangeRestrict a⁻¹ * φ.rangeRestrict b = 1
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x y : R
h : (sInf S).toSetoid x y
r : Setoid R
x✝ : r ∈ (fun x ↦ x.toSetoid) '' S
c : RingCon R
hS : c ∈ S
hr : (fun x ↦ x.toSetoid) c = r
⊢ r x y

Tactic:
rw [← hr]

Goal state after:
R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x y : R
h : (sInf S).toSetoid x y
r : Setoid R
x✝ : r ∈ (fun x ↦ x.toSetoid) '' S
c : RingCon R
hS : c ∈ S
hr : (fun x ↦ x.toSetoid) c = r
⊢ ((fun x ↦ x.toSetoid) c) x y
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: case hex
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∃ x_1, x * x_1 = 1

Tactic:
exact hf.mul_inv_cancel hx

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ ↑f.range
⊢ f.ker ≤ span R (⇑f ⁻¹' s)

Tactic:
let y := Classical.choose h₀

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ ↑f.range
y : M₂ := Classical.choose h₀
⊢ f.ker ≤ span R (⇑f ⁻¹' s)