mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
y : α
hy : y ∈ s
⊢ y ≤ t.sup id

Tactic:
rw [eq_of_le_of_not_lt (Finset.sup_mono (t.subset_insert y))
        (hm _ ⟨insert y t, by simp [Set.insert_subset_iff, hy, ht₁]⟩)]

Goal state after:
case refine_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
y : α
hy : y ∈ s
⊢ y ≤ (insert y t).sup id
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R✝ : Type u
S✝ : Type v
A : Type w
B : Type u₁
M✝ : Type v₁
inst✝¹³ : CommSemiring R✝
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R✝ A
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module A M✝
inst✝⁷ : IsScalarTower R✝ A M✝
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Ring S
inst✝⁴ : AddCommGroup M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
h : Function.Surjective ⇑(algebraMap R S)
N : Submodule R M
⊢ ∀ (c : S) {x : M}, x ∈ N.carrier → c • x ∈ N.carrier

Tactic:
by simpa [h.forall] using N.2

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

Goal state before:
pp: case insert
F : Type u_8
α : Type u_9
β : Type u_10
ι : Type u_11
inst✝⁴ : FunLike F α β
inst✝³ : CommMonoid β
inst✝² : CommMonoid F
inst✝¹ : IsOneApply F α β
inst✝ : IsMulApply F α β
f : ι → F
x : α
i : ι
s : Finset ι
his : i ∉ s
h : (∏ i ∈ s, f i) x = ∏ i ∈ s, (f i) x
⊢ (∏ i ∈ insert i s, f i) x = ∏ i ∈ insert i s, (f i) x

Tactic:
| insert i s his h =>

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
motive : M → Prop
x : M
hx : x ∈ ⨆ i, (p i).toAddSubmonoid
mem : ∀ (i : ι), ∀ x ∈ p i, motive x
zero : motive 0
add : ∀ (x y : M), motive x → motive y → motive (x + y)
⊢ motive x

Tactic:
exact AddSubmonoid.iSup_induction (x := x) _ hx mem zero add

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport f
this : g x = 1
⊢ (f * g) x = f x

Tactic:
rw [Pi.mul_apply, this, mul_one]

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

Goal state before:
pp: case inl
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
x : α
ha : x ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
hx : x ∈ s ∨ x = x
⊢ Disjoint x (sSup ((s ∪ {x}) \ {x}))

pp: case inr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))

Tactic:
· simp only [Set.mem_singleton, Set.insert_sdiff_of_mem, Set.union_singleton]
      exact con.mono_right ((sSup_le_sSup Set.sdiff_subset).trans le_sup_right)

Goal state after:
case inr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))
Module: Mathlib.Data.List.Find

Goal state before:
pp: α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : l₁ ~ l₂
hp : {x | x ∈ l₁ ∧ p x = true}.Subsingleton
⊢ find? p l₁ = find? p l₂

Tactic:
induction h with
  | nil => rfl
  | cons x _ ih =>
    grind
  | swap x y l =>
    dsimp [Set.Subsingleton] at hp
    by_cases p x <;> by_cases p y <;> grind
  | trans _ _ ih1 ih2 =>
    refine (ih1 ?_).trans (ih2 ?_) <;> grind

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_4
inst✝² : CommSemiring R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
s : Finset κ
g : ι → κ → R
⊢ ∑ f ∈ piFinset fun x ↦ s, ∏ i, g i (f i) = ∏ i, ∑ j ∈ s, g i j

Tactic:
by
  rw [← prod_univ_sum]

Goal state after:
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✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
s : Set M
f g : M →ₛₗ[σ₁₂] M₂
⊢ Set.EqOn ⇑f ⇑g ↑(span R s) ↔ Set.EqOn (⇑f) (⇑g) s

Tactic:
← le_eqLocus,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
s : Set M
f g : M →ₛₗ[σ₁₂] M₂
⊢ span R s ≤ f.eqLocus g ↔ Set.EqOn (⇑f) (⇑g) s
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (f + single a b)
a✝⁴ : ι
a✝³ : M
a✝² : ι →₀ M
H : ∀ c ∈ a✝².support, c < a✝⁴
a✝¹ : a✝³ ≠ 0
a✝ : motive a✝²
⊢ single a✝⁴ a✝³ + a✝² = a✝² + single a✝⁴ a✝³

Tactic:
have := fun c hc ↦ (H c hc).ne

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (f + single a b)
a✝⁴ : ι
a✝³ : M
a✝² : ι →₀ M
H : ∀ c ∈ a✝².support, c < a✝⁴
a✝¹ : a✝³ ≠ 0
a✝ : motive a✝²
this : ∀ c ∈ a✝².support, c ≠ a✝⁴
⊢ single a✝⁴ a✝³ + a✝² = a✝² + single a✝⁴ a✝³
Module: Mathlib.Data.Finsupp.Option

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

Tactic:
simp [optionElim]

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

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

Tactic:
simp [optionElim]

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
⊢ s.indicator (fun j ↦ f j * g j) i = s.indicator f i * g i

Tactic:
simp only [indicator]
  split_ifs
  · rfl
  · rw [zero_mul]

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

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : DecidableEq α
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ (f + g).prod h = f.prod h * g.prod h

Tactic:
Finsupp.prod_of_support_subset f subset_union_left h h_zero,

Goal state after:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : DecidableEq α
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ (f + g).prod h = (∏ x ∈ f.support ∪ g.support, h x (f x)) * g.prod h
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
g : α → M → N
n₁ n₂ : N
a : α
ha : a ∈ f.support
h : g a (f a) * n₁ = g a (f a) * n₂
⊢ f.prod g * n₁ = f.prod g * n₂

Tactic:
exact Finset.prod_mul_eq_prod_mul_of_exists a ha h

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
α : Type u_2
s : Multiset α
f : α → R
h : ∀ (a : α), a ∈ s → 1 ≤ f a
⊢ 1 ≤ (map f s).prod

Tactic:
refine one_le_prod fun r hr ↦ ?_
  obtain ⟨a, ha, rfl⟩ := mem_map.mp hr
  exact h a ha

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
⊢ filter p f = f ↔ ∀ (x : α), f x ≠ 0 → p x

Tactic:
simp only [DFunLike.ext_iff, filter_eq_indicator, Set.indicator_apply_eq_self, Set.mem_ofPred_eq,
    not_imp_comm]

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
inst✝ : Nontrivial M
s t : Set α
h : Disjoint (supported M R s) (supported M R t)
x : α
hx1 : x ∈ s
hx2 : x ∈ t
y : M
hy : y ≠ 0
this : single x y = 0
⊢ False

Tactic:
single_eq_zero

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
h : Disjoint (supported M R s) (supported M R t)
x : α
hx1 : x ∈ s
hx2 : x ∈ t
y : M
hy : y ≠ 0
this : y = 0
⊢ False
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ⇑Equiv.plift.symm '' mulSupport f
⊢ mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map Equiv.plift.symm.toEmbedding s)

Tactic:
A,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ⇑Equiv.plift.symm '' mulSupport f
⊢ ⇑Equiv.plift.symm '' mulSupport f ⊆ ↑(Finset.map Equiv.plift.symm.toEmbedding s)
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ val '' Iic i = Iic ↑i

Tactic:
by
  rw [← preimage_val_Iic_val, image_preimage_eq_of_subset]
  simp [range_val]

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

Goal state before:
pp: α : Type u_1
M₀ : Type u_7
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
f : α → M₀
h : ∀ (i : α), f i ≠ 0
⊢ ∏ᶠ (i : α), f i ≠ 0

Tactic:
by
  by_cases h₂ : Set.Finite f.mulSupport
  · grind [finprod_eq_prod f h₂, Finset.prod_ne_zero_iff]
  · simp [finprod_of_infinite_mulSupport h₂]

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

Goal state before:
pp: case inl
ι : 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
i : ι
h : b i ∈ range ⇑b
h✝ : Subsingleton R
⊢ b.reindexRange ⟨b i, h⟩ = b i

pp: case inr
ι : 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
i : ι
h : b i ∈ range ⇑b
h✝ : Nontrivial R
⊢ b.reindexRange ⟨b i, h⟩ = b i

Tactic:
· let := Module.subsingleton R M
    simp [reindexRange, eq_iff_true_of_subsingleton]

Goal state after:
case inr
ι : 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
i : ι
h : b i ∈ range ⇑b
h✝ : Nontrivial R
⊢ b.reindexRange ⟨b i, h⟩ = b i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
x : α
⊢ f x = 1 ∧ g x = 1 → f x * g x = 1

Tactic:
rintro ⟨hf, hg⟩

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf✝ : HasFiniteMulSupport f
hg✝ : HasFiniteMulSupport g
x : α
hf : f x = 1
hg : g x = 1
⊢ f x * g x = 1
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : ¬(s ∩ mulSupport fun x ↦ f (g x)).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)

Tactic:
rw [finprod_mem_eq_one_of_infinite hs, finprod_mem_eq_one_of_infinite]

Goal state after:
case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : ¬(s ∩ mulSupport fun x ↦ f (g x)).Finite
⊢ (g '' s ∩ mulSupport f).Infinite
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n✝ n : ℕ
inst✝ : NeZero n
x✝ : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
h1 : 0 ≤ ↑r
h2 : ↑r < ↑n
⊢ 0 + q = q ∧ ↑(Fin.ofNat n (↑r % ↑n).toNat) = r

Tactic:
emod_eq_of_lt h1 h2,

Goal state after:
m n✝ n : ℕ
inst✝ : NeZero n
x✝ : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
h1 : 0 ≤ ↑r
h2 : ↑r < ↑n
⊢ 0 + q = q ∧ ↑(Fin.ofNat n (↑r).toNat) = r
Module: Mathlib.Algebra.Group.ModEq

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

Tactic:
simpa using (modEq_refl a).add_iff_left (d := 0)

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

Goal state before:
pp: a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
⊢ (0 + (a ^ (c - b) - 1) % (a ^ b - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1

Tactic:
zero_add,

Goal state after:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
⊢ (a ^ (c - b) - 1) % (a ^ b - 1) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

Tactic:
rw [← Nat.sub_add_cancel h, add_mod_right, this, add_mod, mul_mod, mod_self,
        mul_zero, zero_mod, zero_add, mod_mod, pow_sub_one_mod_pow_sub_one]

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

Goal state before:
pp: n a b : ℕ
⊢ (↑b - ↑a) % ↑n = 0 ↔ ↑n ∣ ↑b - ↑a

Tactic:
Int.dvd_iff_emod_eq_zero

Goal state after:
n a b : ℕ
⊢ (↑b - ↑a) % ↑n = 0 ↔ (↑b - ↑a) % ↑n = 0
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
⊢ a ≡ b [MOD m / m.gcd c]

Tactic:
have hcd := gcd_dvd_right m c

Goal state after:
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ a ≡ b [MOD m / m.gcd c]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
⊢ a ≡ b [MOD m / m.gcd c]

Tactic:
let d := gcd m c
  have hmd := gcd_dvd_left m c
  have hcd := gcd_dvd_right m c
  rw [modEq_iff_dvd]
  refine @Int.dvd_of_dvd_mul_right_of_gcd_one (m / d) (c / d) (b - a) ?_ ?_
  · show (m / d : ℤ) ∣ c / d * (b - a)
    rw [mul_comm, ← Int.mul_ediv_assoc (b - a) (Int.natCast_dvd_natCast.mpr hcd), mul_comm]
    apply Int.ediv_dvd_ediv (Int.natCast_dvd_natCast.mpr hmd)
    rw [Int.mul_sub]
    exact modEq_iff_dvd.mp h
  · show Int.gcd (m / d) (c / d) = 1
    simp only [d, ← Int.natCast_div, Int.gcd_natCast_natCast (m / d) (c / d),
      gcd_div hmd hcd, Nat.div_self (gcd_pos_of_pos_left c hm)]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ n)
⊢ (fun f ↦ ⟨∑ i, ↑(f i) * m ^ ↑i, ⋯⟩) ((fun a b ↦ ⟨↑a / m ^ ↑b % m, ⋯⟩) a) = a

Tactic:
by
      dsimp
      induction n with
      | zero => subsingleton [(finCongr <| pow_zero _).subsingleton]
      | succ n ih =>
        simp_rw [Fin.forall_iff, Fin.ext_iff] at ih
        ext
        simp_rw [Fin.sum_univ_succ, Fin.val_zero, Fin.val_succ, pow_zero, Nat.div_one,
          mul_one, pow_succ', ← Nat.div_div_eq_div_mul, mul_left_comm _ m, ← mul_sum]
        rw [ih _ (Nat.div_lt_of_lt_mul (a.is_lt.trans_eq (pow_succ' _ _))), Nat.mod_add_div]

Goal state after:
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) - ↑m * n.gcdB m = ↑n * n.gcdA m
⊢ ↑m ∣ 0 + ↑m * n.gcdB m * ((↑b - ↑a) / ↑(n.gcd m))

pp: case right.refine_1.hcb
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) - ↑m * n.gcdB m = ↑n * n.gcdA m
⊢ ↑(n.gcd m) ∣ ↑m * n.gcdB m * (↑b - ↑a)

Tactic:
zero_add,

Goal state after:
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) - ↑m * n.gcdB m = ↑n * n.gcdA m
⊢ ↑m ∣ ↑m * n.gcdB m * ((↑b - ↑a) / ↑(n.gcd m))

case right.refine_1.hcb
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) - ↑m * n.gcdB m = ↑n * n.gcdA m
⊢ ↑(n.gcd m) ∣ ↑m * n.gcdB m * (↑b - ↑a)
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case neg
m : ℕ
ih : ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
him : ¬iv < m
⊢ ↑(Sum.elim (Fin.castAdd (n (Fin.last m))) (Fin.natAdd (∑ i, n i.castSucc))
        ((finSigmaFinEquiv.sumCongr
            (Equiv.uniqueSigma fun i ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i)))))
          ((Equiv.sumSigmaDistrib fun a ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)))
            ⟨Fin.addCases Sum.inl Sum.inr ⟨iv, hi⟩, ⋯ ▸ j⟩))) =
    ∑ x, n (Fin.castLE ⋯ x) + ↑j

Tactic:
replace him := Nat.eq_of_lt_succ_of_not_lt hi him
    subst him
    conv in Sigma.mk _ _ =>
      equals ⟨Sum.inr 0, j⟩ => simp [Fin.addCases, Fin.natAdd]
    simp
    rfl

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

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
⊢ ↑(a % b).natAbs < ↑b.natAbs

Tactic:
by
      rw [Int.natAbs_of_nonneg (Int.emod_nonneg _ b0), ← Int.abs_eq_natAbs]
      exact Int.emod_lt_abs _ b0

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

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : LinearOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : AddRightReflectLE R
inst✝¹ : IsCancelAdd M
inst✝ : DecidableEq ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i → ∀ i ∈ s, f i = 0
t : Finset ↑↑s
f : ↑↑s → R
heq : ∑ i ∈ t, f i • v ↑i = ∑ i ∈ tᶜ, f i • v ↑i
i : ↑↑s
⊢ ∑ i ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) t, (if h : i ∈ s then f ⟨i, h⟩ else 0) • v i =
    ∑ i ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) Finset.univ \ Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) t,
      (if h : i ∈ s then f ⟨i, h⟩ else 0) • v i

Tactic:
rw [← Finset.map_sdiff]

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : LinearOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : AddRightReflectLE R
inst✝¹ : IsCancelAdd M
inst✝ : DecidableEq ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i → ∀ i ∈ s, f i = 0
t : Finset ↑↑s
f : ↑↑s → R
heq : ∑ i ∈ t, f i • v ↑i = ∑ i ∈ tᶜ, f i • v ↑i
i : ↑↑s
⊢ ∑ i ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) t, (if h : i ∈ s then f ⟨i, h⟩ else 0) • v i =
    ∑ i ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) (Finset.univ \ t), (if h : i ∈ s then f ⟨i, h⟩ else 0) • v i
Module: Mathlib.GroupTheory.MonoidLocalization.Finite

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : Monoid.FG M
hS : S.FG
⊢ Monoid.FG (Localization S)

Tactic:
← Monoid.fg_iff_submonoid_fg

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : Monoid.FG M
hS : Monoid.FG ↥S
⊢ Monoid.FG (Localization S)
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ ¬LinearIndependent R v ↔ ∃ s g, ∑ i ∈ s, g i • v i = 0 ∧ ∃ i ∈ s, g i ≠ 0

Tactic:
rw [linearIndependent_iff']

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ (¬∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0) ↔
    ∃ s g, ∑ i ∈ s, g i • v i = 0 ∧ ∃ i ∈ s, g i ≠ 0
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: case mp.right
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : z ∈ center A
i✝ j✝ : ι
⊢ z * (b i✝ * b j✝) = z * b i✝ * b j✝ ∧ b i✝ * b j✝ * z = b i✝ * (b j✝ * z)

Tactic:
exact ⟨h.2 _ _, h.3 _ _⟩

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : IsTorsionFree R S
b : Basis ι S M
m : M
h : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
⊢ m ∈ span R (range ⇑b)

Tactic:
rw [← b.linearCombination_repr m, Finsupp.linearCombination_apply S _]

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : IsTorsionFree R S
b : Basis ι S M
m : M
h : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
⊢ ((b.repr m).sum fun i a ↦ a • b i) ∈ span R (range ⇑b)
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
b : ↥t
key : Quotient.mk'' (f (Quotient.mk'' a) * ↑b) = Quotient.mk'' a
⊢ (fun a ↦ (Quotient.map' id ⋯ a, Quotient.map' (fun g ↦ ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a))
      ((fun a ↦ Quotient.map' (fun b ↦ f a.1 * ↑b) ⋯ a.2) (Quotient.mk'' a, Quotient.mk'' b)) =
    (Quotient.mk'' a, Quotient.mk'' b)

Tactic:
simp_rw [Quotient.map'_mk'', id, key, inv_mul_cancel_left]

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

Goal state before:
pp: case inr
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n ≤ t.ncard
ht : t.Finite
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

Tactic:
lift s to Finset α using ht.subset hst

Goal state after:
case inr
α : Type u_1
t : Set α
n : ℕ
hnt : n ≤ t.ncard
ht : t.Finite
s : Finset α
hst : ↑s ⊆ t
hsn : (↑s).ncard ≤ n
⊢ ∃ u, ↑s ⊆ u ∧ u ⊆ t ∧ u.ncard = n
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: H : Type u_2
I : Type u_3
inst✝¹ : Monoid H
inst✝ : Monoid I
G : Submonoid (H × I)
hG₁ : Bijective (Prod.fst ∘ ⇑G.subtype)
hG₂ : Bijective (Prod.snd ∘ ⇑G.subtype)
⊢ ∃ e, G = e.toMonoidHom.mgraph

Tactic:
by
  simpa using MonoidHom.exists_mulEquiv_mrange_eq_mgraph hG₁.surjective hG₂.surjective
    fun _ _ ↦ hG₁.injective.eq_iff.trans hG₂.injective.eq_iff.symm

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
⊢ Subsingleton (RingCon R) ↔ Subsingleton R

Tactic:
← not_nontrivial_iff_subsingleton,

Goal state after:
R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
⊢ ¬Nontrivial (RingCon R) ↔ ¬Nontrivial R