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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x ↦ x ∈ range f
g : α → M
⊢ ∏ᶠ (b : β) (h : b ∈ range f), g (Classical.choose h) = ∏ᶠ (a : α), g a

Tactic:
rw [finprod_dmem, finprod_mem_range hf, finprod_congr fun a => _]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x ↦ x ∈ range f
g : α → M
⊢ ∀ (a : α), (if h' : f a ∈ range f then g (Classical.choose h') else 1) = g a
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
H :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ ∑ i ∈ s, (if i ∈ s then f i else 0) • v i = ∑ i ∈ s, (if i ∈ s then g i else 0) • v i

Tactic:
simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, eq]

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b c d p : M
k l : ℕ
hab : k • p + a = l • p + b
m n : ℕ
hcd : m • p + c = n • p + d
⊢ ∃ m n, m • p + (a + c) = n • p + (b + d)

Tactic:
use k + m, l + n

Goal state after:
case h
M : Type u_1
inst✝ : AddCommMonoid M
a b c d p : M
k l : ℕ
hab : k • p + a = l • p + b
m n : ℕ
hcd : m • p + c = n • p + d
⊢ (k + m) • p + (a + c) = (l + n) • p + (b + d)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case mpr
a b n : ℕ
h : a % n = b % n
⊢ a / n * n + a % n ≡ b / n * n + b % n [PMOD n]

Tactic:
← Nat.nsmul_eq_mul,

Goal state after:
case mpr
a b n : ℕ
h : a % n = b % n
⊢ (a / n) • n + a % n ≡ b / n * n + b % n [PMOD n]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case mpr
a b n : ℕ
h : a % n = b % n
⊢ (a / n) • n + a % n ≡ b / n * n + b % n [PMOD n]

Tactic:
← Nat.nsmul_eq_mul,

Goal state after:
case mpr
a b n : ℕ
h : a % n = b % n
⊢ (a / n) • n + a % n ≡ (b / n) • n + b % n [PMOD n]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c : ℕ
h : a ≡ b [MOD n]
⊢ a * c ≡ b * c [MOD n]

Tactic:
rw [mul_comm a, mul_comm b]

Goal state after:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD n]
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mpr
ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ⊆ w
p : Surjective fun i ↦ ⟨v i, ⋯⟩
⊢ range v = w

Tactic:
have q := congr_arg (fun s => ((↑) : w → M) '' s) p.range_eq

Goal state after:
case mpr
ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ⊆ w
p : Surjective fun i ↦ ⟨v i, ⋯⟩
q : (Subtype.val '' range fun i ↦ ⟨v i, ⋯⟩) = Subtype.val '' univ
⊢ range v = w
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case e'_3
R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s := { toFun := fun x ↦ ⟨↑x, ⋯⟩, inj' := ⋯ }
⊢ (range fun x ↦ id ↑x) = s

Tactic:
simp [f, comp_def]

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

Goal state before:
pp: case e'_4
R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s := { toFun := fun x ↦ ⟨↑x, ⋯⟩, inj' := ⋯ }
⊢ range ((fun x ↦ id ↑x) ∘ ⇑f) = t

Tactic:
simp [f, comp_def]

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

Goal state before:
pp: case succ
ι : Type u_1
M : Type u_2
m : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n✝ : Fin (m + 1) → ℕ
f : (i : Fin (m + 1)) → Fin (n✝ i)
n : Fin m → ℕ
nn : ℕ
⊢ ∀ (f : (i : Fin m) → Fin (n i)) (fn : Fin nn),
    ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) + ↑fn * ∏ j, n j < (∏ i, n i) * nn

Tactic:
f

Goal state after:
case succ
ι : Type u_1
M : Type u_2
m : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n✝ : Fin (m + 1) → ℕ
f✝ : (i : Fin (m + 1)) → Fin (n✝ i)
n : Fin m → ℕ
nn : ℕ
f : (i : Fin m) → Fin (n i)
⊢ ∀ (fn : Fin nn), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) + ↑fn * ∏ j, n j < (∏ i, n i) * nn
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
⊢ (∀ (a : Fin (∏ i, xs i)), ⟨∑ i, (↑a / ∏ j, xs (Fin.castLE ⋯ j)) % xs i * ∏ j, xs (Fin.castLE ⋯ j), ⋯⟩ = a) →
    ∀ (a : Fin (∏ i, Fin.cons x xs i)),
      ⟨∑ i, (↑a / ∏ j, Fin.cons x xs (Fin.castLE ⋯ j)) % Fin.cons x xs i * ∏ j, Fin.cons x xs (Fin.castLE ⋯ j), ⋯⟩ = a

Tactic:
ih

Goal state after:
case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
ih : ∀ (a : Fin (∏ i, xs i)), ⟨∑ i, (↑a / ∏ j, xs (Fin.castLE ⋯ j)) % xs i * ∏ j, xs (Fin.castLE ⋯ j), ⋯⟩ = a
⊢ ∀ (a : Fin (∏ i, Fin.cons x xs i)),
    ⟨∑ i, (↑a / ∏ j, Fin.cons x xs (Fin.castLE ⋯ j)) % Fin.cons x xs i * ∏ j, Fin.cons x xs (Fin.castLE ⋯ j), ⋯⟩ = a
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b m n : ℕ
hmn : m.Coprime n
h : a ≡ b [MOD m] ∧ a ≡ b [MOD n]
⊢ a ≡ b [MOD m * n]

Tactic:
Nat.modEq_iff_dvd,

Goal state after:
a b m n : ℕ
hmn : m.Coprime n
h : ↑m ∣ ↑b - ↑a ∧ a ≡ b [MOD n]
⊢ 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 ∧ a ≡ b [MOD n]
⊢ a ≡ b [MOD m * n]

Tactic:
Nat.modEq_iff_dvd,

Goal state after:
a b m n : ℕ
hmn : m.Coprime n
h : ↑m ∣ ↑b - ↑a ∧ ↑n ∣ ↑b - ↑a
⊢ 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
⊢ a ≡ b [MOD m * n]

Tactic:
Nat.modEq_iff_dvd,

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ ↑(Fintype.card ↑s) = s.encard

Tactic:
by
  simp [encard_eq_coe_toFinset_card]

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

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

Tactic:
obtain ⟨y, z, hne, hs⟩ := h

Goal state after:
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}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : s.encard + k ≤ t.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
⊢ k ≤ (t \ s).encard

Tactic:
rw [← encard_sdiff_add_encard_of_subset hst, add_comm] at hkt

Goal state after:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : k + s.encard ≤ (t \ s).encard + s.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
⊢ k ≤ (t \ s).encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
hc : ∀ a₁ ∈ s, ∀ a₂ ∈ s, a₁ ≠ a₂ → f a₁ ≠ f a₂
this : Function.Injective (MapsTo.restrict f s t hf)
⊢ s.encard ≤ t.encard

Tactic:
let f' : s ↪ t := ⟨hf.restrict, this⟩
    exact f'.encard_le

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

Goal state before:
pp: case succ
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
n : ℕ
rank_ih : (N : Submodule R M) → (∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n) → P N
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n + 1
N' : Submodule R M
N'_le : N' ≤ N
x : M
x_mem : x ∈ N
x_ortho : ∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0
m : ℕ
v : Fin m → ↥N'
hli : LinearIndependent R (Subtype.val ∘ v)
c : R
y : M
hy : y ∈ span R (range (Subtype.val ∘ v))
hc : c • x + y = 0
z : Fin m
⊢ (Subtype.val ∘ v) z ∈ ↑N'

Tactic:
exact (v z).2

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↥H
h : Nat.card ↥H = Nat.card G
this : Finite G
⊢ H = ⊤

Tactic:
exact eq_top_of_le_card _ (Nat.le_of_eq h.symm)

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

Goal state before:
pp: α : Type u_3
⊢ ∅.ncard = 0

Tactic:
by
  rw [ncard_eq_zero]

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:
by
  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.GroupTheory.Congruence.Basic

Goal state before:
pp: case mk.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y✝ : M
f✝ f : M →* P
x y : (ker f).Quotient
a✝¹ a✝ : M
h :
  (kerLift f).mrangeRestrict (Quot.mk (⇑(ker f).toSetoid) a✝¹) =
    (kerLift f).mrangeRestrict (Quot.mk (⇑(ker f).toSetoid) a✝)
⊢ (kerLift f) (Quot.mk (⇑(ker f).toSetoid) a✝¹) = (kerLift f) (Quot.mk (⇑(ker f).toSetoid) a✝)

Tactic:
injections

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

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' p'' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
x : M
f : M →ₛₗ[τ₁₂] M₂
h : f x = 0
⊢ x ∈ f.ker

Tactic:
LinearMap.mem_ker,

Goal state after:
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' p'' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
x : M
f : M →ₛₗ[τ₁₂] M₂
h : f x = 0
⊢ f x = 0
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: case succ
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
⊢ mapQ ?succ.p₂ p (f ^ k) ?succ.hg ∘ₗ p.mapQ ?succ.p₂ f ?succ.hf = (p.mapQ p f h ^ k) ∘ₗ p.mapQ p f h

pp: case succ.p₂
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
⊢ Submodule R M

pp: case succ.hf
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
⊢ p ≤ comap f ?succ.p₂

pp: case succ.hg
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
⊢ ?succ.p₂ ≤ comap (f ^ k) p

Tactic:
ih

Goal state after:
case succ
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
⊢ (p.mapQ p f h ^ k) ∘ₗ p.mapQ p f ?succ.hf = (p.mapQ p f h ^ k) ∘ₗ p.mapQ p f h

case succ.hf
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
⊢ p ≤ comap f p

case succ.hg
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
⊢ p ≤ comap (f ^ k) p
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : IsMin b
⊢ Ioc a (pred b) = Ioo a b

Tactic:
rw [Ioc_eq_empty (hb.mono <| pred_le _).not_lt, Ioo_eq_empty hb.not_lt]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
a : α
⊢ Icc a (pred b) = Ico a b

Tactic:
ext x; rw [mem_Icc, mem_Ico, le_pred_iff_of_not_isMin hb]

Goal state after:
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
b : α
⊢ ↑(Icc (succ a) b) = ↑(Ioc a b)

Tactic:
by simpa using Set.Icc_succ_left_eq_Ioc_of_not_isMax ha _

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁶ : Semiring R✝
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝¹⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝¹⁴ : (i : ι) → Module R✝ (φ i)
inst✝¹³ : (i : ι) → AddCommMonoid (ψ i)
inst✝¹² : (i : ι) → Module R✝ (ψ i)
inst✝¹¹ : (i : ι) → AddCommMonoid (χ i)
inst✝¹⁰ : (i : ι) → Module R✝ (χ i)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
⊢ ∀ (x : α ⊕ β → M),
    (Equiv.sumArrowEquivProdArrow α β M).toFun (r • x) = (RingHom.id R) r • (Equiv.sumArrowEquivProdArrow α β M).toFun x

Tactic:
f

Goal state after:
R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁶ : Semiring R✝
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝¹⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝¹⁴ : (i : ι) → Module R✝ (φ i)
inst✝¹³ : (i : ι) → AddCommMonoid (ψ i)
inst✝¹² : (i : ι) → Module R✝ (ψ i)
inst✝¹¹ : (i : ι) → AddCommMonoid (χ i)
inst✝¹⁰ : (i : ι) → Module R✝ (χ i)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
f : α ⊕ β → M
⊢ (Equiv.sumArrowEquivProdArrow α β M).toFun (r • f) = (RingHom.id R) r • (Equiv.sumArrowEquivProdArrow α β M).toFun f
Module: Mathlib.Data.Fintype.Pigeonhole

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
⊢ ∃ y, Infinite ↑(f ⁻¹' {y})

Tactic:
by
  classical
    by_contra! hf
    cases nonempty_fintype β
    let key : Fintype α :=
      { elems := univ.biUnion fun y : β => (f ⁻¹' {y}).toFinset
        complete := by simp }
    exact key.false

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ x_1, f x_1 = x) ↔ f' x.1 = x.2
s : S
h : H
⊢ (↑f').toFun (s • h) = (RingHom.id S) s • (↑f').toFun h

Tactic:
simp only [ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, RingHom.id_apply]

Goal state after:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ x_1, f x_1 = x) ↔ f' x.1 = x.2
s : S
h : H
⊢ f' (s • h) = s • f' h
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ x_1, f x_1 = x) ↔ f' x.1 = x.2
s : S
h : H
⊢ (h, f' h) ∈ f.range

Tactic:
rw [LinearMap.mem_range, hf']

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ (∏ i ∈ Ioc m n, f i) * ∏ i ∈ Ioc n k, f i = ∏ i ∈ Ioc m k, f i

Tactic:
rw [← Ioc_union_Ioc_eq_Ioc hmn hnk, prod_union]

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ Disjoint (Ioc m n) (Ioc n k)
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝ : Monoid A
⊢ ∀ (a b : HasMulAntidiagonal A), a = b

Tactic:
by
    rintro ⟨a, ha⟩ ⟨b, hb⟩
    congr with n xy
    rw [ha, hb]

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

Goal state before:
pp: δ : Type u_4
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ (∏ k ∈ Ico m n, f k) * ∏ k ∈ range m, f k = ∏ k ∈ range n, f k

Tactic:
(rw [mul_comm]; exact prod_range_mul_prod_Ico f h)

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

Goal state before:
pp: M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∑ i ∈ Ico a b, ∑ j ∈ Ico i b, f i j = ∑ j ∈ Ico a b, ∑ i ∈ Ico a (j + 1), f i j

Tactic:
Finset.sum_sigma',

Goal state after:
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∑ x ∈ (Ico a b).sigma fun i ↦ Ico i b, f x.fst x.snd = ∑ j ∈ Ico a b, ∑ i ∈ Ico a (j + 1), f i j
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∑ i ∈ Ico a b, ∑ j ∈ Ico (i + 1) b, f i j = ∑ j ∈ Ico a b, ∑ i ∈ Ico a j, f i j

Tactic:
Finset.sum_sigma',

Goal state after:
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∑ x ∈ (Ico a b).sigma fun i ↦ Ico (i + 1) b, f x.fst x.snd = ∑ j ∈ Ico a b, ∑ i ∈ Ico a j, f i j
Module: Mathlib.Data.List.NatAntidiagonal

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
⊢ x ∈ antidiagonal n ↔ x.fst + x.snd = n

Tactic:
rcases x with ⟨x, y⟩
  simp [antidiagonal]
  grind

Goal state after:
Module: Mathlib.RingTheory.Ideal.Defs

Goal state before:
pp: α : Type u
inst✝¹ : Ring α
I : Ideal α
a b c d : α
inst✝ : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d = a * c - b * c + b * (c - d)

Tactic:
mul_sub

Goal state after:
α : Type u
inst✝¹ : Ring α
I : Ideal α
a b c d : α
inst✝ : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d = a * c - b * c + (b * c - b * d)
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : q * q - p * q - (q * p - p * p) = q - p
⊢ Commute p q

Tactic:
hp.eq,

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : q * q - p * q - (q * p - p) = q - p
⊢ Commute p q
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
x y x✝ : α
⊢ x✝ * y = x ↔ x = y * x✝

Tactic:
rw [eq_comm, mul_comm]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: case isUnit_or_isUnit.refine_1.a
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
c d : α
ha : a = a * c * (a * d)
huv : ¬IsUnit (a * c) ∧ ¬IsUnit (a * d)
⊢ a * (c * d) ∣ a

pp: case a
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
c d : α
ha : a = a * c * (a * d)
huv : ¬IsUnit (a * c) ∧ ¬IsUnit (a * d)
⊢ a ∣ a * (c * d)

Tactic:
· exact (dvd_mul_right (a * (c * d)) a).trans (ha.trans (by ring)).symm.dvd

Goal state after:
case a
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
c d : α
ha : a = a * c * (a * d)
huv : ¬IsUnit (a * c) ∧ ¬IsUnit (a * d)
⊢ a ∣ a * (c * d)
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ I.IsMaximal

Tactic:
apply Ideal.isMaximal_iff.2
  constructor
  · intro h
    rcases hqf.exists_pair_ne with ⟨⟨x⟩, ⟨y⟩, hxy⟩
    exact hxy (Ideal.Quotient.eq.2 (mul_one (x - y) ▸ I.mul_mem_left _ h))
  · intro J x hIJ hxnI hxJ
    rcases hqf.mul_inv_cancel (mt Ideal.Quotient.eq_zero_iff_mem.1 hxnI) with ⟨⟨y⟩, hy⟩
    rw [← zero_add (1 : R), ← sub_self (x * y), sub_add]
    exact J.sub_mem (J.mul_mem_right _ hxJ) (hIJ (Ideal.Quotient.eq.1 hy))

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

Goal state before:
pp: ι : Type u_2
inst✝⁴ : LinearOrder ι
α : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : LocallyFiniteOrder ι
inst✝¹ : SuccOrder ι
inst✝ : OrderBot ι
f : ι → α
i : ι
⊢ (partialSups f) (Order.succ i) = f ⊥ ⊔ (partialSups (f ∘ Order.succ)) i

Tactic:
by
  refine Succ.rec (by simp) (fun j _ h ↦ ?_) (bot_le (a := i))
  have : (partialSups (f ∘ Order.succ)) (Order.succ j) =
      ((partialSups (f ∘ Order.succ)) j ⊔ (f ∘ Order.succ) (Order.succ j)) := by simp
  simp [this, h, sup_assoc]

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

Goal state before:
pp: case succ
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective ⇑f
hi : Injective ⇑i
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
⊢ comap f (map i (f.iterateMapComap i n K)) = comap f (map i (f.iterateMapComap i (n + 1) K))

Tactic:
ih

Goal state after:
case succ
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective ⇑f
hi : Injective ⇑i
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
⊢ comap f (map i (f.iterateMapComap i (n + 1) K)) = comap f (map i (f.iterateMapComap i (n + 1) K))
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
p : α → Submodule R M
i : α
x : M
hx : x ∈ p i
j : α
⊢ ((lsingle i) x) j ∈ p j

Tactic:
rcases eq_or_ne i j with rfl|h <;> simp_all

Goal state after: