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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ ∏ x ∈ s, (f x + -g x) = ∏ i ∈ s, f i + -∑ x ∈ s, (g x * ∏ x ∈ s with x < x, (f x + -g x)) * ∏ i ∈ s with x < i, f i

Tactic:
convert! prod_add_ordered s f fun i => -g i

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ -∑ x ∈ s, (g x * ∏ x ∈ s with x < x, (f x + -g x)) * ∏ i ∈ s with x < i, f i =
    ∑ i ∈ s, (-g i * ∏ j ∈ s with j < i, (f j + -g j)) * ∏ j ∈ s with i < j, f j
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s : Finset ι
f : ι →₀ M
hf : f.support = ∅
⊢ motive f

Tactic:
support_eq_empty.1 hf

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s : Finset ι
f : ι →₀ M
hf : f.support = ∅
⊢ motive 0
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case inr
R : Type u_3
S : Type u_4
inst✝⁴ : Field R
inst✝³ : Semifield S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : ExistsAddOfLE S
v : AbsoluteValue R S
x : R
hx₀ : x ≠ 0
hx₁ : v x ≠ 1
h : 1 < v x
⊢ ∃ x, 1 < v x

Tactic:
· exact ⟨x, h⟩

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

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s : Multiset α
a : α
inst✝ : MulLeftMono α
h : ∀ (x : α), x ∈ s → a ≤ x
⊢ a ^ s.card ≤ s.prod

Tactic:
← Multiset.prod_replicate,

Goal state after:
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s : Multiset α
a : α
inst✝ : MulLeftMono α
h : ∀ (x : α), x ∈ s → a ≤ x
⊢ (replicate s.card a).prod ≤ s.prod
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ≃ β
a : α
b : M
⊢ equivMapDomain f (single a b) = single (f a) b

Tactic:
classical
    ext x
    simp only [single_apply, ← Equiv.eq_symm_apply, equivMapDomain_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
f : α ≃ β
⊢ (α →₀ M) ≃ (β →₀ M)

Tactic:
refine ⟨equivMapDomain f, equivMapDomain f.symm, fun f => ?_, fun f => ?_⟩ <;> ext x <;>
    simp only [equivMapDomain_apply, Equiv.symm_symm, Equiv.symm_apply_apply,
      Equiv.apply_symm_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : α →₀ M
⊢ (mapDomain (⇑f) x).support = map f x.support

Tactic:
ext b
  simp only [mem_support_iff, ne_eq, mem_map]
  refine ⟨fun h ↦ ?_, ?_⟩
  · obtain ⟨a, rfl⟩ := mem_range_of_mapDomain_ne_zero h
    exact ⟨a, by simpa [f.injective] using h⟩
  · rintro ⟨a, ha, rfl⟩
    simpa [f.injective]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : AddZeroClass α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ (erase i f + single i a).sum g + g i (f i) = f.sum g + g i a

Tactic:
sum_add_index' hg hgg

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : AddZeroClass α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ (erase i f).sum g + (single i a).sum g + g i (f i) = f.sum g + g i a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
b : β
hb : b ∉ Set.range f
m : M
hf : Set.InjOn f (f ⁻¹' ↑(single b m).support)
a : α
⊢ b = f a → m = 0

Tactic:
rintro rfl

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
m : M
a : α
hb : f a ∉ Set.range f
hf : Set.InjOn f (f ⁻¹' ↑(single (f a) m).support)
⊢ m = 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α × β →₀ M
⊢ f.curry.support = image Prod.fst f.support

Tactic:
by unfold Finsupp.curry; congr!

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

Goal state before:
pp: α : Type u_1
R : Type u_6
inst✝ : MulZeroOneClass R
a : α
b : R
⊢ b • single a 1 = single a b

Tactic:
rw [smul_single, smul_eq_mul, mul_one]

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

Goal state before:
pp: case refine_1
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
⊢ (fun i ↦ single i 1) '' s ⊆ ↑(supported R R s)

Tactic:
rintro _ ⟨_, hp, rfl⟩
    exact single_mem_supported R 1 hp

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
s t : Set α
⊢ ⨅ i, supported M R (bif i then s else t) = supported M R s ⊓ supported M R t

Tactic:
iInf_bool_eq

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
⊢ supported M R (bif true then s else t) ⊓ supported M R (bif false then s else t) = supported M R s ⊓ supported M R t
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

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
v : α → M
h : Function.Surjective v
⊢ Function.Surjective ⇑(linearCombination R v)

Tactic:
intro x
  obtain ⟨y, hy⟩ := h x
  exact ⟨single y 1, by simp [hy]⟩

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 : M
i : ι
a✝ : Nontrivial R
⊢ ∀ (c : R) (x : M), (fun i ↦ (b.reindexRange.repr (c • x)) ⟨b i, ⋯⟩) = c • fun i ↦ (b.reindexRange.repr x) ⟨b i, ⋯⟩

Tactic:
intro c x
    ext i
    simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
⊢ ⊤ ≤ span R (Set.range v) ↔ ∀ (x : M), ∃ c, ∑ i, c i • v i = x

Tactic:
← mem_span_range_iff_exists_fun

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
⊢ ⊤ ≤ span R (Set.range v) ↔ ∀ (x : M), x ∈ span R (Set.range v)
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
inst✝ : Fintype ι
⊢ ⇑b.sumCoords = ⇑(∑ i, b.coord i)

Tactic:
ext m

Goal state after:
ι : 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
inst✝ : Fintype ι
m : M
⊢ b.sumCoords m = (∑ i, b.coord i) m
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
⊢ ⇑b.sumCoords = fun m ↦ ∑ᶠ (i : ι), (b.coord i) m

Tactic:
ext m

Goal state after:
ι : 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
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
m : M
s : Set M
⊢ (∃ n f g, ∑ i, f i • ↑(g i) = m) → m ∈ span R s

Tactic:
rintro ⟨n, f, g, rfl⟩

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
n : ℕ
f : Fin n → R
g : Fin n → ↑s
⊢ ∑ i, f i • ↑(g i) ∈ span R s
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 : Set M
⊢ ↑(span R s) = ⋃ n, (fun f ↦ ∑ i, (f i).1 • (f i).2) '' {f | ∀ (i : Fin n), (f i).2 ∈ s}

Tactic:
ext m

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
⊢ m ∈ ↑(span R s) ↔ m ∈ ⋃ n, (fun f ↦ ∑ i, (f i).1 • (f i).2) '' {f | ∀ (i : Fin n), (f i).2 ∈ s}
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ insert a s), f i = f a * ∏ᶠ (i : α) (_ : i ∈ s), f i

Tactic:
insert_eq,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ {a} ∪ s), f i = f a * ∏ᶠ (i : α) (_ : i ∈ s), f i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
⊢ Disjoint {a} s

Tactic:
rwa [disjoint_singleton_left]

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
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : b ∈ mulSupport fun b ↦ ∏ a ∈ s with g a = b, f a
⊢ b ∈ g '' ↑s

Tactic:
suffices {a ∈ s | g a = b}.Nonempty by
    simpa only [fiber_nonempty_iff_mem_image, Finset.mem_image, exists_prop]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : b ∈ mulSupport fun b ↦ ∏ a ∈ s with g a = b, f a
⊢ {a ∈ s | g a = b}.Nonempty
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: case succ
n✝ n : ℕ
i : Fin (n + 1)
k : Fin n
ih : (finCycle k.castSucc) i = (⇑(finRotate (n + 1)))^[↑k] i
⊢ ↑((finCycle k.succ) i) = ↑((⇑(finRotate (n + 1)))^[↑k + 1] i)

Tactic:
Function.iterate_succ',

Goal state after:
case succ
n✝ n : ℕ
i : Fin (n + 1)
k : Fin n
ih : (finCycle k.castSucc) i = (⇑(finRotate (n + 1)))^[↑k] i
⊢ ↑((finCycle k.succ) i) = ↑((⇑(finRotate (n + 1)) ∘ (⇑(finRotate (n + 1)))^[↑k]) i)
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n i : ℕ
h : i + 1 < n + 1 + 1
x hd : M
tl : Fin n → M
i_lt : i < n + 1
i_fin : Fin (n + 1) := ⟨i, i_lt⟩
⊢ ∏ j, i_fin.succ.insertNth x (cons hd tl) j = x * ∏ j, cons hd tl j

Tactic:
simp only [insertNth_succ_cons, prod_cons]

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
n i : ℕ
h : i + 1 < n + 1 + 1
x hd : M
tl : Fin n → M
i_lt : i < n + 1
i_fin : Fin (n + 1) := ⟨i, i_lt⟩
⊢ hd * ∏ i, i_fin.insertNth x tl i = x * (hd * ∏ i, tl i)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case mpr
a b n : ℕ
⊢ a ≡ b [MOD n] → a ≡ b [PMOD n]

Tactic:
· rw [Nat.ModEq]
    intro h
    rw [← Nat.div_add_mod' a n, ← Nat.div_add_mod' b n, ← Nat.nsmul_eq_mul, ← Nat.nsmul_eq_mul, h]
    exact nsmul_add_modEq _ |>.trans (nsmul_add_modEq _).symm

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

Goal state before:
pp: R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
f : M →ₗ[R] M'
hs : LinearIndepOn R id s
hf_inj : InjOn ⇑f ↑(span R s)
⊢ InjOn ⇑f ↑(span R (id '' s))

Tactic:
by simpa using hf_inj

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

Goal state before:
pp: ι : 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
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h :
  ∀ (s t : Finset ι) (f : ι → R),
    Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
| ∑ i ∈ s with g i ≤ f i, (if g i ≤ f i then f i - g i else g i - f i) • v i +
    (∑ i ∈ s with g i ≤ f i, g i • v i + ∑ i ∈ s with f i < g i, f i • v i)

Tactic:
rw [← add_assoc, ← Finset.sum_add_distrib]

Goal state after:
ι : 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
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h :
  ∀ (s t : Finset ι) (f : ι → R),
    Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
| ∑ x ∈ s with g x ≤ f x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + g x • v x) +
    ∑ i ∈ s with f i < g i, f i • v i
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b m n : ℕ
hmn : m.Coprime n
h : m ∣ (↑b - ↑a).natAbs ∧ ↑n ∣ ↑(↑b - ↑a).natAbs
⊢ a ≡ b [MOD m * n]

Tactic:
Int.natCast_dvd_natCast

Goal state after:
a b m n : ℕ
hmn : m.Coprime n
h : m ∣ (↑b - ↑a).natAbs ∧ n ∣ (↑b - ↑a).natAbs
⊢ a ≡ b [MOD m * n]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b m n : ℕ
hmn : m.Coprime n
h : m ∣ (↑b - ↑a).natAbs ∧ n ∣ (↑b - ↑a).natAbs
⊢ ↑(m * n) ∣ ↑(↑b - ↑a).natAbs

Tactic:
Int.natCast_dvd_natCast

Goal state after:
a b m n : ℕ
hmn : m.Coprime n
h : m ∣ (↑b - ↑a).natAbs ∧ n ∣ (↑b - ↑a).natAbs
⊢ m * n ∣ (↑b - ↑a).natAbs
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
⊢ card α ≤ card β

Tactic:
rw [← card_ulift α, ← card_ulift β]

Goal state after:
α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
⊢ card (ULift.{?u.15, u_3} α) ≤ card (ULift.{?u.17, u_4} β)
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
⊢ Module.rank R M = 1

Tactic:
rw [Module.rank_def, ciSup_eq_of_forall_le_of_forall_lt_exists_gt]
  · have := Module.subsingleton R M
    simp [Set.subsingleton_of_subsingleton]
  · intro w hw
    exact ⟨⟨{0}, LinearIndepOn.of_subsingleton⟩, hw.trans_eq (Cardinal.mk_singleton _).symm⟩

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

Goal state before:
pp: R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R' →+* R
j : S →+* S'
hi : Injective ⇑i
hj : Injective ⇑j
hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S'
⊢ lift.{v', v} (Module.rank R S) ≤ lift.{v, v'} (Module.rank R' S')

Tactic:
refine _root_.lift_rank_le_of_injective_injectiveₛ i j hi hj fun r _ ↦ ?_

Goal state after:
R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R' →+* R
j : S →+* S'
hi : Injective ⇑i
hj : Injective ⇑j
hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S'
r : R'
x✝ : S
⊢ ↑j (i r • x✝) = r • ↑j x✝
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R →+* R'
j : S →+* S'
hi : Surjective ⇑i
hj : Injective ⇑j
hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)
⊢ lift.{v', v} (Module.rank R S) ≤ lift.{v, v'} (Module.rank R' S')

Tactic:
refine _root_.lift_rank_le_of_surjective_injective i j hi hj fun r _ ↦ ?_
  have := congr($hc r)
  simp only [RingHom.coe_comp, comp_apply] at this
  simp only [smul_def, AddMonoidHom.coe_coe, map_mul, this]

Goal state after:
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
hv : LinearIndependent R v
f g : ι →₀ R
h : (f.sum fun a b ↦ b • v a) = g.sum fun a b ↦ b • v a
⊢ f = g

Tactic:
ext m

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
hv : LinearIndependent R v
f g : ι →₀ R
h : (f.sum fun a b ↦ b • v a) = g.sum fun a b ↦ b • v a
m : ι
⊢ f m = g m
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ (s \ {a}).encard + 1 = s.encard

Tactic:
by
  rw [← encard_insert_of_notMem (fun h ↦ h.2 rfl), insert_sdiff_singleton, insert_eq_of_mem h]

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

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ a ≠ b

Tactic:
rintro rfl

Goal state after:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hb : a ∈ s
⊢ False
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
a : α
ha : a ∈ s
⊢ (s \ {a}).encard = k

Tactic:
rw [encard_sdiff_singleton_of_mem ha, h,
      (ENat.addLECancellable_of_ne_top ENat.one_ne_top).add_tsub_cancel_right]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ ¬1 ≤ s.encard ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ x, s = {x}

Tactic:
Order.one_le_iff_ne_zero,

Goal state after:
α : Type u_1
s : Set α
⊢ ¬s.encard ≠ 0 ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ x, s = {x}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
h : s \ {x} = {y}
⊢ x ≠ y

Tactic:
rintro rfl

Goal state after:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
h : s \ {x} = {x}
⊢ False
Module: Mathlib.Data.Set.Card

Goal state before:
pp: 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

Tactic:
rintro rfl

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

Goal state before:
pp: 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

Tactic:
rintro rfl

Goal state after:
case refine_1.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
hne : y ≠ x
hs : s \ {x} = {y, x}
⊢ False
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1.refine_1
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ x ≠ y

Tactic:
rintro rfl

Goal state after:
case refine_1.refine_1
α : Type u_1
s : Set α
x : α
hx : x ∈ s
z w : α
hzw : z ≠ w
hyz : x ≠ z
hyw : x ≠ w
hs : s \ {x} = {x, z, w}
⊢ False
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ x ≠ z

Tactic:
rintro rfl

Goal state after:
case refine_1.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y w : α
hyw : y ≠ w
hyz : y ≠ x
hzw : x ≠ w
hs : s \ {x} = {y, x, w}
⊢ False
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y w : α
hyw : y ≠ w
hyz : y ≠ x
hzw : x ≠ w
hs : s \ {x} = {y, x, w}
⊢ False

Tactic:
exact (hs.symm.subset (Or.inr (Or.inl rfl))).2 rfl

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

Goal state before:
pp: case refine_1.refine_3
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ x ≠ w

Tactic:
rintro rfl

Goal state after:
case refine_1.refine_3
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hyz : y ≠ z
hyw : y ≠ x
hzw : z ≠ x
hs : s \ {x} = {y, z, x}
⊢ False
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = ↑n
hk : ↑n + 1 ≤ s.encard
⊢ t₀ ≠ s

Tactic:
rintro rfl

Goal state after:
α : Type u_1
n : ℕ
t₀ : Set α
ht₀ : t₀.encard = ↑n
IH : ↑n ≤ t₀.encard → ∃ t ⊆ t₀, t.encard = ↑n
ht₀s : t₀ ⊆ t₀
hk : ↑n + 1 ≤ t₀.encard
⊢ False
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H = ⊥ → Nat.card ↥H = 1

Tactic:
rintro rfl

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ Nat.card ↥⊥ = 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.ncard ≠ 0
⊢ s ≠ ∅

Tactic:
rintro rfl

Goal state after:
α : Type u_1
hs : ∅.ncard ≠ 0
⊢ False
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ (s \ {a}).ncard + 1 = s.ncard

Tactic:
by
  to_encard_tac
  rw [hs.cast_ncard_eq, hs.sdiff.cast_ncard_eq, encard_sdiff_singleton_add_one h]

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
A : Subgroup G
B : Subgroup H
q : (G ⧸ A) × H ⧸ B
⊢ ∀ (a₁ : G) (a₂ : H) (b₁ : G) (b₂ : H), (leftRel A) a₁ b₁ → (leftRel B) a₂ b₂ → ↑(a₁, a₂) = ↑(b₁, b₂)

Tactic:
simp [QuotientGroup.leftRel_apply, Subgroup.mem_prod, QuotientGroup.eq, ← and_imp]

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

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

Tactic:
exact ConGen.Rel.symm (h fb fa)

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

Goal state before:
pp: α : Type u_4
M : Type u_5
inst✝² : MulOneClass M
inst✝¹ : SMul α M
inst✝ : IsScalarTower α M M
c : Con M
a : α
w x : M
h : c w x
⊢ c (a • w) (a • x)

Tactic:
simpa only [smul_one_mul] using c.mul (c.refl' (a • (1 : M) : M)) h

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
p : Submodule R M
⊢ p = ⊤ → Nonempty (Unique (M ⧸ p))

Tactic:
rintro rfl

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Nonempty (Unique (M ⧸ ⊤))
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]; exact h c hS

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
i : ι
hi : i ∈ I
b : φ i
j : ι
hj : j ∈ J
⊢ j ≠ i

Tactic:
rintro rfl

Goal state after:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
j : ι
hj : j ∈ J
hi : j ∈ I
b : φ j
⊢ False
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
p p' : Submodule R M
H : p ≤ p'
⊢ Function.Surjective ⇑(factor H)

Tactic:
by
  intro x
  use Quotient.mk x.out
  exact Quotient.out_eq x

Goal state after: