mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case neg
α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
s✝ : Multiset (α →₀ M)
a : α
f : α →₀ M
s : Multiset (α →₀ M)
ih : a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support
h : a ∉ f.support
ha : s.sum a ≠ 0
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support

Tactic:
rcases ih (mem_support_iff.2 ha) with ⟨f', h₀, h₁⟩

Goal state after:
case neg
α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
s✝ : Multiset (α →₀ M)
a : α
f : α →₀ M
s : Multiset (α →₀ M)
ih : a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support
h : a ∉ f.support
ha : s.sum a ≠ 0
f' : α →₀ M
h₀ : f' ∈ s
h₁ : a ∈ f'.support
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
⊢ ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x

Tactic:
classical calc
    ∏ x ∈ s, f x = (∏ x ∈ s with f x = 1, f x) * ∏ x ∈ s with f x ≠ 1, f x := by
      rw [← prod_union, filter_union_filter_not_eq]
      exact disjoint_filter.2 fun _ _ h n_h ↦ n_h h
    _ ≤ ∏ x ∈ t, f x :=
      mul_le_of_le_one_of_le
        (prod_le_one' <| by simp only [mem_filter, and_imp]; exact fun _ _ ↦ le_of_eq)
        (prod_le_prod_of_subset' <| by simpa only [subset_iff, mem_filter, and_imp])

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

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
x : PLift α
h : x ∈ mulSupport fun x ↦ (fun x ↦ 1) x.down
⊢ x ∈ ↑∅

Tactic:
by simp at h

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
⊢ map (lmapDomain M R f) (supported M R s) = supported M R (f '' s)

Tactic:
cases isEmpty_or_nonempty α

Goal state after:
case inl
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
h✝ : IsEmpty α
⊢ map (lmapDomain M R f) (supported M R s) = supported M R (f '' s)

case inr
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
h✝ : Nonempty α
⊢ map (lmapDomain M R f) (supported M R s) = supported M R (f '' s)
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : l ∈ (lmapDomain M R f).ker
⊢ l ∈ ⊥

Tactic:
mem_ker,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (lmapDomain M R f) l = 0
⊢ l ∈ ⊥
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this✝ : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
this : (l.sum fun a ↦ single (f a)) (f x) = 0
⊢ l x = 0 x

Tactic:
rw [Finsupp.sum_apply, Finsupp.sum_eq_single x, single_eq_same] at this

Goal state after:
case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this✝ : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
this : l x = 0
⊢ l x = 0 x

case pos.h₀
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this✝ : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
this : (l.sum fun a₁ b ↦ (single (f a₁) b) (f x)) = 0
⊢ ∀ (b : α), l b ≠ 0 → b ≠ x → (single (f b) (l b)) (f x) = 0

case pos.h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this✝ : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
this : (l.sum fun a₁ b ↦ (single (f a₁) b) (f x)) = 0
⊢ l x = 0 → (single (f x) 0) (f x) = 0
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: case pos.h₀
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this✝ : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
this : (l.sum fun a₁ b ↦ (single (f a₁) b) (f x)) = 0
⊢ ∀ (b : α), l b ≠ 0 → b ≠ x → (single (f b) (l b)) (f x) = 0

pp: case pos.h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this✝ : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
this : (l.sum fun a₁ b ↦ (single (f a₁) b) (f x)) = 0
⊢ l x = 0 → (single (f x) 0) (f x) = 0

Tactic:
· intro y hy xy
      simp only [SetLike.mem_coe, mem_supported, subset_def, mem_support_iff] at h₁
      simp [mt (H _ (h₁ _ hy) _ xs) xy]

Goal state after:
case pos.h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this✝ : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
this : (l.sum fun a₁ b ↦ (single (f a₁) b) (f x)) = 0
⊢ l x = 0 → (single (f x) 0) (f x) = 0
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
x : M
hx : x ∈ v '' s
⊢ x ∈ ↑(map (linearCombination R v) (supported R R s))

Tactic:
Set.mem_image

Goal state after:
case h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
x : M
hx : ∃ x_1 ∈ s, v x_1 = x
⊢ x ∈ ↑(map (linearCombination R v) (supported R R s))
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
⊢ ∀ {x : α}, f x ≠ 1 → (x ∈ s ↔ x ∈ t)

Tactic:
intro x hxf
    rw [← mem_mulSupport] at hxf
    refine ⟨fun hx => ?_, fun hx => ?_⟩
    · refine ((mem_inter_iff x t (mulSupport f)).mp ?_).1
      rw [← Set.ext_iff.mp h x, mem_inter_iff]
      exact ⟨hx, hxf⟩
    · refine ((mem_inter_iff x s (mulSupport f)).mp ?_).1
      rw [Set.ext_iff.mp h x, mem_inter_iff]
      exact ⟨hx, hxf⟩

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

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x y : M
⊢ x = y ↔ ∀ (i : ι), (b.repr x) i = (b.repr y) i

Tactic:
by
  simp only [← DFunLike.ext_iff, EmbeddingLike.apply_eq_iff_eq]

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

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f (b i) = ⇑(single i 1)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun x ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
j : ι
⊢ (b.repr (b j)) i = f (b j) i

Tactic:
rw [b.repr_self, f_eq]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Finset α
⊢ (∏ᶠ (i : α) (_ : i ∈ ↑s ∪ ↑t), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ ↑t), f i =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑t), f i

Tactic:
← Finset.coe_union,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Finset α
⊢ (∏ᶠ (i : α) (_ : i ∈ ↑(s ∪ t)), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ ↑t), f i =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑t), f i
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
x : M
⊢ x ∈ span R ↑s → ∃ f, Function.support f ⊆ ↑s ∧ ∑ a ∈ s, f a • a = x

Tactic:
rw [mem_span_iff_exists_finset_subset]
    rintro ⟨f, t, hts, hf, rfl⟩
    refine ⟨f, hf.trans hts, .symm <| Finset.sum_subset hts ?_⟩
    simp +contextual [Function.support_subset_iff'.1 hf]

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

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
m : M
⊢ b.sumCoords m = ∑ᶠ (i : ι), (b.coord i) m

Tactic:
simp only [Basis.sumCoords, Basis.coord, Finsupp.lapply_apply, LinearMap.id_coe,
    LinearEquiv.coe_coe, Function.comp_apply, Finsupp.coe_lsum, LinearMap.coe_comp,
    finsum_eq_sum _ (b.repr m).hasFiniteSupport, Finsupp.sum, Finset.finite_toSet_toFinset, id,
    Finsupp.fun_support_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
g : β → M
e : α → β
he₀ : Bijective e
he₁ : ∀ (x : α), f x = g (e x)
⊢ ∏ᶠ (i : α) (_ : i ∈ univ), f i = ∏ᶠ (j : β), g j

Tactic:
← finprod_mem_univ g

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
g : β → M
e : α → β
he₀ : Bijective e
he₁ : ∀ (x : α), f x = g (e x)
⊢ ∏ᶠ (i : α) (_ : i ∈ univ), f i = ∏ᶠ (i : β) (_ : i ∈ univ), g i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
⊢ r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a

Tactic:
by_cases hr : r = 0
  · simp_all
  by_cases h : f.support.Finite
  · exact mul_finsum' f r h
  simp [finsum_def, HasFiniteSupport, h, (by aesop : (r * f ·).support = f.support)]

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

Goal state before:
pp: case inr
n✝ n : ℕ
i : Fin (n + 2)
h : i < Fin.last (n + 1)
⊢ (finRotate (n + 2)) i = i + 1

Tactic:
· cases i
      simp only [Fin.lt_def, Fin.val_last] at h
      simp [finRotate_of_lt h, Fin.add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ h)]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ i < (finRotate n) i ↔ i ≠ -1

Tactic:
obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (NeZero.ne n)

Goal state after:
n : ℕ
inst✝ : NeZero n.succ
i : Fin n.succ
⊢ i < (finRotate n.succ) i ↔ i ≠ -1
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ (Equiv.symm (finRotate n)) i < i ↔ i ≠ 0

Tactic:
obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (NeZero.ne n)

Goal state after:
n : ℕ
inst✝ : NeZero n.succ
i : Fin n.succ
⊢ (Equiv.symm (finRotate n.succ)) i < i ↔ i ≠ 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hf_inj : InjOn ⇑f ↑(span R (Set.range v))
⊢ LinearIndependent R (⇑f ∘ v) ↔ LinearIndependent R v

Tactic:
by
  simp_rw [LinearIndependent, Finsupp.linearCombination_linear_comp, coe_comp]
  rw [hf_inj.injective_iff]
  rw [← Finsupp.range_linearCombination, LinearMap.coe_range]

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

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a ↦ a • v i) = g.sum fun i a ↦ a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a ↦ a • v ↑i) = l₂.sum fun i a ↦ a • v ↑i
⊢ ∀ x ∈ (Finsupp.embDomain (Embedding.subtype fun x ↦ x ∈ s) l₁).support, x ∈ s

pp: case refine_2
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a ↦ a • v i) = g.sum fun i a ↦ a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a ↦ a • v ↑i) = l₂.sum fun i a ↦ a • v ↑i
⊢ ∀ x ∈ (Finsupp.embDomain (Embedding.subtype fun x ↦ x ∈ s) l₂).support, x ∈ s

pp: case refine_3
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a ↦ a • v i) = g.sum fun i a ↦ a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a ↦ a • v ↑i) = l₂.sum fun i a ↦ a • v ↑i
⊢ ((Finsupp.embDomain (Embedding.subtype fun x ↦ x ∈ s) l₁).sum fun i a ↦ a • v i) =
    (Finsupp.embDomain (Embedding.subtype fun x ↦ x ∈ s) l₂).sum fun i a ↦ a • v i

Tactic:
iterate 2 simpa using fun _ h _ ↦ h

Goal state after:
case refine_3
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a ↦ a • v i) = g.sum fun i a ↦ a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a ↦ a • v ↑i) = l₂.sum fun i a ↦ a • v ↑i
⊢ ((Finsupp.embDomain (Embedding.subtype fun x ↦ x ∈ s) l₁).sum fun i a ↦ a • v i) =
    (Finsupp.embDomain (Embedding.subtype fun x ↦ x ∈ s) l₂).sum fun i a ↦ a • v i
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin (n + 1) → G
x✝ : Fin (n + 1)
x : Fin n
hx : f 0 * partialProd (fun i ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc = f x.castSucc
⊢ f 0 * partialProd (fun i ↦ (f i.castSucc)⁻¹ * f i.succ) x.succ = f x.succ

Tactic:
rw [partialProd_succ, ← mul_assoc, hx, mul_inv_cancel_left]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: n : ℕ
⊢ Coprime 1 n ↔ True

Tactic:
simp [Coprime]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: n : ℕ
⊢ n.Coprime 1 ↔ True

Tactic:
simp [Coprime]

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c : ℕ
h : a % n = b % n
⊢ c * a % (c * n) = c * b % (c * n)

Tactic:
mul_mod_mul_left,

Goal state after:
n a b c : ℕ
h : a % n = b % n
⊢ c * (a % n) = c * b % (c * n)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c : ℕ
h : a % n = b % n
⊢ c * (a % n) = c * b % (c * n)

Tactic:
mul_mod_mul_left,

Goal state after:
n a b c : ℕ
h : a % n = b % n
⊢ c * (a % n) = c * (b % n)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case succ
n a b : ℕ
h : a ≡ b [MOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [MOD n]
⊢ a ^ (d + 1) ≡ b ^ (d + 1) [MOD n]

Tactic:
rw [Nat.pow_succ, Nat.pow_succ]

Goal state after:
case succ
n a b : ℕ
h : a ≡ b [MOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [MOD n]
⊢ a ^ d * a ≡ b ^ d * b [MOD n]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : c ≡ d [MOD n]
⊢ ↑n ∣ ↑(b + d) - ↑(a + c)

Tactic:
Int.natCast_add,

Goal state after:
n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : c ≡ d [MOD n]
⊢ ↑n ∣ ↑b + ↑d - ↑(a + c)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : c ≡ d [MOD n]
⊢ ↑n ∣ ↑b + ↑d - ↑(a + c)

Tactic:
Int.natCast_add,

Goal state after:
n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : c ≡ d [MOD n]
⊢ ↑n ∣ ↑b + ↑d - (↑a + ↑c)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case right.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ ↑m ∣ ↑b - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m)

Tactic:
rw [← sub_eq_iff_eq_add] at this
          rw [← this, Int.sub_mul, sub_add, ← Int.mul_sub, Int.sub_ediv_of_dvd,
            Int.mul_ediv_cancel_left _ hnonzero, Int.mul_ediv_assoc _ h.dvd, ← sub_add, sub_self,
            zero_add, mul_assoc]
          · exact dvd_mul_right _ _
          · exact hcoedvd _

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : Disjoint s t
⊢ ENat.card ↑(s ∪ t) = ENat.card ↑s + ENat.card ↑t

Tactic:
simp [ENat.card_congr (Equiv.Set.union h)]

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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (s \ t).encard + (s ∩ t).encard = s.encard

Tactic:
rw [← encard_union_eq disjoint_sdiff_inter, sdiff_union_inter]

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

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card ↑t ≤ ENat.card ↑s
this : ENat.card ↑t ≤ 0 + ENat.card ↑s
⊢ ENat.card ↑(t \ s) + ENat.card ↑s ≤ 0 + ENat.card ↑s

Tactic:
rwa [← ENat.card_sum, ← ENat.card_congr <| Equiv.Set.union disjoint_sdiff_left,
      sdiff_union_of_subset hsub.subset]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
H : Type u_2
inst✝ : Group H
f : α →* H
a x✝ : α
⊢ f x✝ = f a ↔ a⁻¹ • x✝ ∈ f.ker

Tactic:
mem_ker,

Goal state after:
α : Type u_1
inst✝¹ : Group α
H : Type u_2
inst✝ : Group H
f : α →* H
a x✝ : α
⊢ f x✝ = f a ↔ f (a⁻¹ • x✝) = 1
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 : φ a = φ b
⊢ a⁻¹ * b ∈ φ.ker

Tactic:
mem_ker,

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 : φ a = φ b
⊢ φ (a⁻¹ * b) = 1
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
⊢ a⁻¹ * b ∈ φ.rangeRestrict.ker

Tactic:
mem_ker,

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⁻¹ * b) = 1
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H✝ : Type v
inst✝¹ : Group H✝
M : Type x
inst✝ : Monoid M
φ✝ : G →* H✝
H N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
⊢ ∀ (a : ↥(H ⊔ N)), ∃ a_1, φ a_1 = Quotient.mk'' a

Tactic:
rintro ⟨y, hy : y ∈ (H ⊔ N)⟩
      rw [← SetLike.mem_coe] at hy
      rw [coe_mul_of_left_le_normalizer_right H N hLE] at hy
      rcases hy with ⟨h, hh, n, hn, rfl⟩
      simp only [SetLike.mem_coe] at hn
      use ⟨h, hh⟩
      refine Quotient.eq.mpr ?_
      simp [leftRel_apply, inclusion, mem_subgroupOf, hn]

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Nonempty α
hs : s.Finite
⊢ (∃ x, s ⊆ ↑{x}) ↔ ∃ x, s ⊆ {x}

Tactic:
Finset.coe_singleton

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

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M✝ : Type x
inst✝ : Monoid M✝
φ : G →* H
M : Subgroup G
nM : M.Normal
h : N ≤ M
x : G
hx : x ∈ ↑M
⊢ (mk' N) x ∈ (map N M (MonoidHom.id G) h).ker

Tactic:
mem_ker,

Goal state after:
G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M✝ : Type x
inst✝ : Monoid M✝
φ : G →* H
M : Subgroup G
nM : M.Normal
h : N ≤ M
x : G
hx : x ∈ ↑M
⊢ (map N M (MonoidHom.id G) h) ((mk' N) x) = 1
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocRing R
N : AddSubgroup R
inst✝ : N.Normal
n : ℤ
a : R
⊢ ↑(↑n * a) = n • ↑a

Tactic:
← zsmul_eq_mul,

Goal state after:
R : Type u_1
inst✝¹ : NonAssocRing R
N : AddSubgroup R
inst✝ : N.Normal
n : ℤ
a : R
⊢ ↑(n • a) = n • ↑a
Module: Mathlib.LinearAlgebra.Quotient.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
h : p = p'
⊢ ∀ (m : R) (x : M ⧸ p),
    (Quotient.congr (Equiv.refl M) ⋯).toFun (m • x) = (RingHom.id R) m • (Quotient.congr (Equiv.refl M) ⋯).toFun x

Tactic:
rintro x ⟨y⟩
      rfl

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

Goal state before:
pp: case mul
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ ⦃a b : M⦄, f a = w → f b = x → (conGen fun x y ↦ rel (f x) (f y)) a b
ih1 : ∀ ⦃a b : M⦄, f a = y → f b = z → (conGen fun x y ↦ rel (f x) (f y)) a b
a b : M
fa : f a = w * y
fb : f b = x * z
⊢ (conGen fun x y ↦ rel (f x) (f y)) a b

Tactic:
← f.eq_symm_apply,

Goal state after:
case mul
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ ⦃a b : M⦄, f a = w → f b = x → (conGen fun x y ↦ rel (f x) (f y)) a b
ih1 : ∀ ⦃a b : M⦄, f a = y → f b = z → (conGen fun x y ↦ rel (f x) (f y)) a b
a b : M
fa : a = f.symm (w * y)
fb : b = f.symm (x * z)
⊢ (conGen fun x y ↦ rel (f x) (f y)) a b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : pred a ≤ b
x : α
⊢ x ∈ insert (pred a) (Icc a b) ↔ x ∈ Icc (pred a) b

Tactic:
simp [or_and_left, pred_le_iff_eq_or_le]

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : pred a ≤ b
x : α
⊢ x = pred a ∨ a ≤ x → x = pred a → x ≤ b
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrderTop α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Ici (a + 1) = Ioi a

Tactic:
by
  simpa [succ_eq_add_one] using Ici_succ_eq_Ioi a

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∏ i, ∏ j > i, f j i * f i j = ∏ x, (∏ x_1 > x, f x_1 x) * ∏ x_1 < x, f x_1 x

Tactic:
prod_mul_distrib

Goal state after:
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ (∏ x, ∏ x_1 > x, f x_1 x) * ∏ x, ∏ x_1 > x, f x x_1 = (∏ x, ∏ x_1 > x, f x_1 x) * ∏ x, ∏ x_1 < x, f x_1 x
Module: Mathlib.Data.List.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal (n + 2) = (0, n + 2) :: map (Prod.map Nat.succ Nat.succ) (antidiagonal n) ++ [(n + 2, 0)]

Tactic:
rw [antidiagonal_succ', antidiagonal_succ]
  simp

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

Goal state before:
pp: n : ℕ
⊢ #(antidiagonal n) = n + 1

Tactic:
by simp [antidiagonal]

Goal state after: