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

Goal state before:
pp: S : Type u_5
inst✝³ : Ring S
inst✝² : PartialOrder S
R : Type u_6
inst✝¹ : Ring R
abv : R → S
inst✝ : IsAbsoluteValue abv
a b c : R
⊢ abv (a - c) ≤ abv (a - b) + abv (b - c)

Tactic:
by
  simpa [sub_eq_add_neg, add_assoc] using abv_add abv (a - b) (b - c)

Goal state after:
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✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ ∏ j ∈ s, f j < ∏ j ∈ t, f j

Tactic:
by
  classical calc
    ∏ j ∈ s, f j < ∏ j ∈ insert i s, f j := by
      rw [prod_insert hs]
      exact lt_mul_of_one_lt_left' (∏ j ∈ s, f j) hlt
    _ ≤ ∏ j ∈ t, f j := by
      apply prod_le_prod_of_subset_of_one_le'
      · simp [Finset.insert_subset_iff, h, ht]
      · intro x hx h'x
        simp only [mem_insert, not_or] at h'x
        exact hle x hx h'x.2

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

Goal state before:
pp: ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
⊢ ∀ (a : (i : ι) × αs i),
    a ∈ l.support ↔ a ∈ (image Sigma.fst l.support).sigma fun i ↦ l.support.preimage (Sigma.mk i) ⋯

Tactic:
Sigma.forall,

Goal state after:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
⊢ ∀ (a : ι) (b : αs a),
    ⟨a, b⟩ ∈ l.support ↔ ⟨a, b⟩ ∈ (image Sigma.fst l.support).sigma fun i ↦ l.support.preimage (Sigma.mk i) ⋯
Module: Mathlib.Data.Finsupp.SMulWithZero

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

Tactic:
ext i; exact zero_smul _ _

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

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_7
R : Type u_11
S : Type u_12
inst✝³ : Zero M
inst✝² : SMulZeroClass R M
inst✝¹ : Zero N
inst✝ : SMulZeroClass S N
f : M → N
hf : f 0 = 0
c : R
d : S
v : α →₀ M
hsmul : ∀ (x : M), f (c • x) = d • f x
a✝ : α
⊢ (mapRange f hf (c • v)) a✝ = (d • mapRange f hf v) a✝

Tactic:
simp [hsmul]

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

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
hf : HasFiniteMulSupport (f ∘ PLift.down)
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
x : PLift α
x✝ : x ∈ s
hxf : x ∉ mulSupport (f ∘ PLift.down)
⊢ f x.down = 1

Tactic:
notMem_mulSupport

Goal state after:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
hf : HasFiniteMulSupport (f ∘ PLift.down)
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
x : PLift α
x✝ : x ∈ s
hxf : (f ∘ PLift.down) x = 1
⊢ f x.down = 1
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.sum fun a ↦ single (f a)) = 0
x : α
⊢ l x = 0 x

Tactic:
have := Classical.decPred fun x => x ∈ s

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₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this : DecidablePred fun x ↦ x ∈ s
⊢ l x = 0 x
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
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
c : α
⊢ z c • v c ∈ span R (v '' s)

Tactic:
have := Classical.decPred fun x => x ∈ s

Goal state after:
α : 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 α
z : α →₀ R
hz : z ∈ supported R R s
c : α
this : DecidablePred fun x ↦ x ∈ s
⊢ z c • v c ∈ span R (v '' s)
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' := ⋯ }
this : lapply i ∘ₗ ↑b.repr = f_i
⊢ (b.repr x) i = f x i

Tactic:
calc
    b.repr x i = f_i x := by
      { rw [← this]
        rfl }
    _ = f x i := rfl

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

Goal state before:
pp: M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : 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✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
i : ι
⊢ ((b.constr S) f) (b i) = f i

Tactic:
by
  simp [Basis.constr_apply, b.repr_self]

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Finset α
x✝ : ∃ c, ∑ i, c i • v ↑i = x
c : ↥s → R
hc : ∑ i, c i • v ↑i = x
⊢ ∑ i ∈ s, (fun i ↦ if h : i ∈ s then c ⟨i, h⟩ else 0) i • v i = x

Tactic:
← hc,

Goal state after:
case refine_1
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Finset α
x✝ : ∃ c, ∑ i, c i • v ↑i = x
c : ↥s → R
hc : ∑ i, c i • v ↑i = x
⊢ ∑ i ∈ s, (fun i ↦ if h : i ∈ s then c ⟨i, h⟩ else 0) i • v i = ∑ i, c i • v ↑i
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case refine_2
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Finset α
x✝ : ∃ c, ∑ i ∈ s, c i • v i = x
c : α → R
hc : ∑ i ∈ s, c i • v i = x
⊢ ∑ i, (fun i ↦ c ↑i) i • v ↑i = x

Tactic:
← hc,

Goal state after:
case refine_2
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Finset α
x✝ : ∃ c, ∑ i ∈ s, c i • v i = x
c : α → R
hc : ∑ i ∈ s, c i • v i = x
⊢ ∑ i, (fun i ↦ c ↑i) i • v ↑i = ∑ i ∈ s, c i • v i
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: case cons
α : Type u_1
n✝ : ℕ
inst✝ : DecidableEq α
a : α
n : ℕ
x : α
xs : List.Vector α n
hxs : #{i | xs.get i = a} = List.count a xs.toList
⊢ (if x = a then 1 else 0) + #{x | xs.get x = a} = List.count a (x :: xs.toList)

Tactic:
hxs,

Goal state after:
case cons
α : Type u_1
n✝ : ℕ
inst✝ : DecidableEq α
a : α
n : ℕ
x : α
xs : List.Vector α n
hxs : #{i | xs.get i = a} = List.count a xs.toList
⊢ (if x = a then 1 else 0) + List.count a xs.toList = List.count a (x :: xs.toList)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∈ mulSupport f
⊢ f a ∣ finprod f

pp: case neg
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∉ mulSupport f
⊢ f a ∣ finprod f

Tactic:
· rw [finprod_eq_prod_of_mulSupport_toFinset_subset f hf (Set.Subset.refl _)]
    exact Finset.dvd_prod_of_mem f ((Finite.mem_toFinset hf).mpr ha)

Goal state after:
case neg
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∉ mulSupport f
⊢ f a ∣ finprod f
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) = ↑((finCycle k.castSucc) i + 1)

Tactic:
finCycle_apply,

Goal state after:
case succ
n✝ n : ℕ
i : Fin (n + 1)
k : Fin n
ih : (finCycle k.castSucc) i = (⇑(finRotate (n + 1)))^[↑k] i
⊢ ↑(i + k.succ) = ↑((finCycle k.castSucc) i + 1)
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
⊢ ↑(i + k.succ) = ↑((finCycle k.castSucc) i + 1)

Tactic:
finCycle_apply,

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

Goal state before:
pp: x y z : ℕ∞
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
rcases eq_or_ne y 0 with y_0 | y_0

Goal state after:
case inl
x y z : ℕ∞
y_0 : y = 0
⊢ x ^ (y * z) = (x ^ y) ^ z

case inr
x y z : ℕ∞
y_0 : y ≠ 0
⊢ x ^ (y * z) = (x ^ y) ^ z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.inr.inl
y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
⊢ 1 ^ (y * z) = (1 ^ y) ^ z

Tactic:
simp only [one_epow]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 7 → M
⊢ ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6

Tactic:
by
  rw [prod_univ_castSucc, prod_univ_six]
  rfl

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n ≤ m
f : Fin m → M
a b : Fin n
⊢ ∏ i ∈ Icc (castLE h a) (castLE h b), f i = ∏ i ∈ Icc a b, f (castLE h i)

Tactic:
simp [← map_castLEEmb_Icc]

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

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
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r₁ r₂ : ι → R'
s : ι
hs : s ∈ S
H : ∑ x ∈ S, r₁ x • j (v x) = ∑ x ∈ S, r₂ x • j (v x)
⊢ r₁ s = r₂ s

Tactic:
← hc,

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
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r₁ r₂ : ι → R'
s : ι
hs : s ∈ S
H : ∑ x ∈ S, j (i (r₁ x) • v x) = ∑ x ∈ S, j (i (r₂ x) • v x)
⊢ r₁ s = r₂ s
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:
by
    simp only [Pi.smul_apply, smul_eq_mul] at hx ⊢
    rw [partialProd_succ, ← mul_assoc, hx, mul_inv_cancel_left]

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

Goal state before:
pp: case inr.inr
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
    j.contractNth (fun x1 x2 ↦ x1 * x2) g k

Tactic:
rwa [succAbove_of_le_castSucc, succAbove_of_le_castSucc, partialProd_succ, partialProd_succ,
      castSucc_succ, partialProd_succ, inv_mul_cancel_left, contractNth_apply_of_gt]

Goal state after:
case inr.inr.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ j ≤ k.castSucc

case inr.inr.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ j.succ ≤ k.castSucc.castSucc
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : m = 0
⊢ b ≡ a [MOD n] ∧ b ≡ b [MOD m]

Tactic:
rw [hm, gcd_zero_right] at h

Goal state after:
m n a b c d : ℕ
h : a ≡ b [MOD n]
hn : ¬n = 0
hm : m = 0
⊢ b ≡ a [MOD n] ∧ b ≡ b [MOD m]
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : ∀ (m : M), j m = 0 → m = 0
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r' : ι → R'
s : ι
hs : s ∈ S
H : ∑ x ∈ S, r' x • j (v x) = 0
⊢ r' s = 0

Tactic:
← hc,

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : ∀ (m : M), j m = 0 → m = 0
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r' : ι → R'
s : ι
hs : s ∈ S
H : ∑ x ∈ S, j (i (r' x) • v x) = 0
⊢ r' s = 0
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case inr
a b n : ℕ
h : b ≤ a % n
hn : n > 0
⊢ a % n - b = (a - b) % n

Tactic:
← div_add_mod a n

Goal state after:
case inr
a b n : ℕ
h : b ≤ a % n
hn : n > 0
⊢ a % n - b = (n * (a / n) + a % n - b) % n
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ Nat.card ↑(graphOn f s) = Nat.card ↑s

Tactic:
← Nat.card_image_of_injOn fst_injOn_graph,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ Nat.card ↑(Prod.fst '' graphOn f s) = Nat.card ↑s
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✝ : Nontrivial R
ι : Type u_1
v : ι → M
s : Set ι
hs : LinearIndepOn R v s
⊢ s.encard ≤ toENat (Module.rank R M)

Tactic:
simpa using OrderHom.mono (β := ℕ∞) Cardinal.toENat hs.linearIndependent.cardinal_lift_le_rank

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

Goal state before:
pp: case pos
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → MulOneClass (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
H : j = i
⊢ (MonoidHom.mulSingle f i) _x j ∈ s j

pp: case neg
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → MulOneClass (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
H : ¬j = i
⊢ (MonoidHom.mulSingle f i) _x j ∈ s j

Tactic:
· subst H
          simpa

Goal state after:
case neg
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → MulOneClass (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
H : ¬j = i
⊢ (MonoidHom.mulSingle f i) _x j ∈ s j
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: case pos
η : Type u_3
f : η → Type u_4
inst✝¹ : (i : η) → Group (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
H : j = i
⊢ (MonoidHom.mulSingle f i) _x j ∈ s j

pp: case neg
η : Type u_3
f : η → Type u_4
inst✝¹ : (i : η) → Group (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
H : ¬j = i
⊢ (MonoidHom.mulSingle f i) _x j ∈ s j

Tactic:
· subst H
          simpa

Goal state after:
case neg
η : Type u_3
f : η → Type u_4
inst✝¹ : (i : η) → Group (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
H : ¬j = i
⊢ (MonoidHom.mulSingle f i) _x j ∈ s j
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: case inr
α : Type u_1
l : List α
h : l.Nodup
h✝ : Infinite α
⊢ ↑l.length ≤ ENat.card α

Tactic:
grw [ENat.card_eq_top_of_infinite]
    exact le_top

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
⊢ s.toFinset.card ≤ t.toFinset.card

Tactic:
{ rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card'] }

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

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s \ t).ncard + t.ncard = (s ∪ t).ncard

Tactic:
rw [← ncard_union_eq disjoint_sdiff_left hs.sdiff ht, sdiff_union_self]

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s.ncard + t.ncard < Nat.card α
⊢ s ∪ t ≠ univ

Tactic:
exact union_ne_univ_of_ncard_add_ncard_lt h

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
c : RingCon R
⊢ c.toCon = ⊤ ↔ c = ⊤

Tactic:
by rw [← toCon_top, toCon_inj]

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 p' : Submodule R M
⊢ map p.mkQ p' = ⊤ ↔ p ⊔ p' = ⊤

Tactic:
simp only [LinearMap.map_eq_top_iff p.range_mkQ, sup_comm, ker_mkQ]

Goal state after:
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: R : Type u
inst✝ : Semiring R
h : IsField R
a : R
ha : a ≠ 0
⊢ (a * if ha : a = 0 then 0 else Classical.choose ⋯) = 1

Tactic:
convert! Classical.choose_spec (h.mul_inv_cancel ha)

Goal state after:
R : Type u
inst✝ : Semiring R
h : IsField R
a : R
ha : a ≠ 0
⊢ (if ha : a = 0 then 0 else Classical.choose ⋯) = Classical.choose ⋯
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
⊢ f.coprod g ∘ₗ inl R M M₂ = f

Tactic:
ext; simp only [map_zero, add_zero, coprod_apply, inl_apply, comp_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : AddCommMonoid M₄
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M₄
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₄
⊢ (f.prodMap g).range = f.range.prod g.range

Tactic:
ext ⟨_, _⟩; simp

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

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

Tactic:
← Set.singleton_subset_iff

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

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
⊢ map (fst R M M₂) (p.prod q) = p

Tactic:
by
  ext x; simp [(⟨0, zero_mem _⟩ : ∃ x, x ∈ q)]

Goal state after:
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
convert! (Finset.sup_inf_distrib_left s.toFinset id a).le using 1

Goal state after:
case e'_4
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨆ b ∈ s, a ⊓ b = s.toFinset.sup fun i ↦ a ⊓ id i
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
a : α
f : ι → α
inst✝¹ : Nonempty ι
inst✝ : Finite ι
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
⊢ (∃ i, a ≤ f i) → a ≤ ⨆ i, f i

Tactic:
rintro ⟨i, hai⟩

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
a : α
f : ι → α
inst✝¹ : Nonempty ι
inst✝ : Finite ι
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
i : ι
hai : a ≤ f i
⊢ a ≤ ⨆ i, f i
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case insert
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
i : ι
hpi : p (f i)
a✝ : ι
s✝ : Finset ι
ht : a✝ ∉ s✝
IH : p (f i \ s✝.sup f)
⊢ p (f i \ (s✝.sup f ⊔ f a✝))

Tactic:
← sdiff_sdiff

Goal state after:
case insert
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
i : ι
hpi : p (f i)
a✝ : ι
s✝ : Finset ι
ht : a✝ ∉ s✝
IH : p (f i \ s✝.sup f)
⊢ p ((f i \ s✝.sup f) \ f a✝)
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case insert
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
i : ι
hpi : p (f i)
a✝ : ι
s✝ : Finset ι
ht : a✝ ∉ s✝
IH : p (f i \ s✝.sup f)
⊢ p ((f i \ s✝.sup f) \ f a✝)

Tactic:
exact hdiff IH

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
⊢ #(Iio x) < n + 1

Tactic:
← hn

Goal state after:
case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
⊢ #(Iio x) < #(Iio i)
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case e'_2.a
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
x✝ : ℕ
a✝ : x✝ ∈ Icc ↑a ↑b
⊢ (if h : x✝ < n then f ⟨x✝, h⟩.succ / f ⟨x✝, h⟩.castSucc else 1) =
    (if hi : x✝ + 1 < n + 1 then f ⟨x✝ + 1, hi⟩ else 1) / if hi : x✝ < n + 1 then f ⟨x✝, hi⟩ else 1

Tactic:
simp_all
    grind

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

Goal state before:
pp: case not_isUnit
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
⊢ ¬IsUnit a

pp: case isUnit_or_isUnit
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
⊢ ∀ ⦃a_1 b : α⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b

Tactic:
· intro ha
    apply max.ne_top
    rw [span_singleton_eq_top.2 ha]

Goal state after:
case isUnit_or_isUnit
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
⊢ ∀ ⦃a_1 b : α⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b