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

Goal state before:
pp: case refine_2
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
⊢ partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = (partialProd g ∘ a.succ.succAbove) i.castSucc →
    partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.succ = (partialProd g ∘ a.succ.succAbove) i.succ

Tactic:
hi

Goal state after:
case refine_2
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = (partialProd g ∘ a.succ.succAbove) i.castSucc
⊢ partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.succ = (partialProd g ∘ a.succ.succAbove) i.succ
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case refine_2
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
⊢ partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc * a.contractNth (fun x1 x2 ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)

Tactic:
hi

Goal state after:
case refine_2
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
⊢ partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun x1 x2 ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b n : ℕ
hn : 0 < n.succ
⊢ (a ^ n.succ).Coprime b ↔ a.Coprime b

Tactic:
Nat.pow_succ,

Goal state after:
a b n : ℕ
hn : 0 < n.succ
⊢ (a ^ n * a).Coprime b ↔ a.Coprime b
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr.inr
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k ∣ m * c
hnc : k ∣ n * c
hm : m > 0
hn : n > 0
⊢ k / m.gcd n ∣ c

Tactic:
simpa [Nat.div_dvd_iff_dvd_mul (Nat.dvd_trans (Nat.gcd_dvd_left m n) hkm)
    (gcd_pos_of_pos_left n hm), Nat.gcd_mul_right m c n] using (Nat.dvd_gcd hmc hnc)

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
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
⊢ v x ∈ R ∙ v x

Tactic:
exact mem_span_singleton_self (v x)

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

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

Tactic:
Nat.pow_succ,

Goal state after:
case succ
n a b : ℕ
h : a ≡ b [MOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [MOD n]
⊢ a ^ d * a ≡ b ^ (d + 1) [MOD n]
Module: Mathlib.Algebra.BigOperators.Fin

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

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_castSucc_lt, succAbove_of_le_castSucc, partialProd_succ,
    castSucc_succ, ← mul_assoc,
      partialProd_right_inv, contractNth_apply_of_eq]
    · simp [le_iff_val_le_val, ← h]
    · rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
      exact le_of_eq h

Goal state after:
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
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c m : ℕ
hc : c ≠ 0
⊢ c * a ≡ c * b [MOD c * m] → a ≡ b [MOD m]

Tactic:
simp only [modEq_iff_dvd, Int.natCast_mul, ← Int.mul_sub]

Goal state after:
a b c m : ℕ
hc : c ≠ 0
⊢ ↑c * ↑m ∣ ↑c * (↑b - ↑a) → ↑m ∣ ↑b - ↑a
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case refine_2
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
i : ι ⊕ ι'
⊢ i ∈ s → g i = 0

Tactic:
hi

Goal state after:
case refine_2
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
i : ι ⊕ ι'
hi : i ∈ s
⊢ g i = 0
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
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
h :
  (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0
i : ι
⊢ i ∈ s → f i = g i

Tactic:
hi

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
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
h :
  (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0
i : ι
hi : i ∈ s
⊢ f i = g i
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case pos
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j with ↑j < i, f j
h : i < n
⊢ (take (i + 1) (ofFn f)).prod = ∏ j with ↑j < i + 1, f j

Tactic:
have : i < length (ofFn f) := by rwa [length_ofFn]
      rw [prod_take_succ _ _ this]
      have A : ({j | j.val < i + 1} : Finset (Fin n)) =
          insert ⟨i, h⟩ ({j | Fin.val j < i} : Finset (Fin n)) := by grind
      grind

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

Goal state before:
pp: case inl
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Nat.card α ≠ 0
val✝ : Fintype α
⊢ α ≃ Fin (Nat.card α)

Tactic:
simpa only [card_eq_fintype_card] using Fintype.equivFin α

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Subsingleton α
⊢ Nat.card α = 1

Tactic:
by
  let := Fintype.ofSubsingleton a
  rw [card_eq_fintype_card, Fintype.card_ofSubsingleton a]

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

Goal state before:
pp: α : Type u_3
⊢ 1 < card α ↔ ↑1 < #α

Tactic:
← natCast_lt_toENat

Goal state after:
α : Type u_3
⊢ 1 < card α ↔ ↑1 < toENat #α
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ g a * 1 = (g a • ⇑a) 1

Tactic:
by rw [← a.map_one]; rfl

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 ι
inst✝ : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
i : ι
⊢ i ∈ t₁ᶜ → i ∉ t₂ → (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) • v i = 0

Tactic:
hi

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 ι
inst✝ : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
i : ι
hi : i ∈ t₁ᶜ
⊢ i ∉ t₂ → (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) • v i = 0
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ gcdA 0 s = 0

Tactic:
unfold gcdA
  rw [xgcd, xgcd_zero_left]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ Module.rank R R = 1

Tactic:
by
  nontriviality R
  rw [le_antisymm_iff, ← not_lt, ← two_le_iff_one_lt, ← Nat.cast_two,
    Module.le_rank_iff_exists_linearMap, Module.one_le_rank_iff]
  refine ⟨fun ⟨f, inj⟩ ↦ ?_, _, (LinearEquiv.refl ..).injective⟩
  have := inj (a₁ := f ![0, 1] • ![1, 0]) (a₂ := f ![1, 0] • ![0, 1]) <| by
    simp_rw [map_smul, smul_eq_mul]; apply mul_comm
  have h₁ : f ![0, 1] = 0 := by simpa using congr($this 0)
  have h₂ : 0 = f ![1, 0] := by simpa using congr($this 1)
  exact zero_ne_one (α := R) (by simpa using congr($(inj (h₁.trans h₂)) 1))

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

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Finite
⊢ s.encard < ⊤

Tactic:
induction s, h using Set.Finite.induction_on with
  | empty => simp
  | insert hat _ ht' =>
    rw [encard_insert_of_notMem hat]
    exact lt_tsub_iff_right.1 ht'

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard ≠ ⊤ ↔ s.Finite

Tactic:
← lt_top_iff_ne_top,

Goal state after:
α : Type u_1
s : Set α
⊢ s.encard < ⊤ ↔ s.Finite
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
⊢ s.encard ≤ t.encard

Tactic:
by
  rw [← union_sdiff_cancel h, encard_union_eq disjoint_sdiff_right]; exact le_self_add

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

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

Tactic:
encard_union_eq disjoint_sdiff_left,

Goal state after:
α : Type u_1
s t : Set α
⊢ (s \ t).encard + t.encard + (s ∩ t).encard = s.encard + t.encard
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
h : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
s : Finset ι
f : ι → R
⊢ (∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0) ↔ ∑ i ∈ s, f i • v i = ∑ i ∈ s, 0 i • v i → ∀ i ∈ s, f i = 0 i

Tactic:
Pi.zero_apply,

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
h : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
s : Finset ι
f : ι → R
⊢ (∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0) ↔ ∑ i ∈ s, f i • v i = ∑ x ∈ s, 0 • v x → ∀ i ∈ s, f i = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard

Tactic:
obtain (h | h) := (s ∪ t).finite_or_infinite
  · to_encard_tac
    rw [h.cast_ncard_eq, (h.subset subset_union_left).cast_ncard_eq,
      (h.subset subset_union_right).cast_ncard_eq]
    apply encard_union_le
  rw [h.ncard]
  apply zero_le

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

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

Tactic:
rw [add_comm]

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
⊢ t.ncard ≤ (t \ s).ncard + s.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
heven : Even (Nat.card α)
s : Set α
⊢ ¬Even sᶜ.ncard ↔ Odd s.ncard

Tactic:
even_ncard_compl_iff heven,

Goal state after:
α : Type u_1
inst✝ : Finite α
heven : Even (Nat.card α)
s : Set α
⊢ ¬Even s.ncard ↔ Odd s.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite ↑s
t' : Finset ↑s
⊢ (Subtype.val '' ↑t').ncard = t'.card

Tactic:
rw [ncard_image_of_injective _ Subtype.coe_injective]

Goal state after:
α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite ↑s
t' : Finset ↑s
⊢ (↑t').ncard = t'.card
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
hs : s.Finite
⊢ s.ncard = n + 1 ↔ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n

Tactic:
by
  refine ⟨eq_insert_of_ncard_eq_succ, ?_⟩
  rintro ⟨a, t, hat, h, rfl⟩
  rw [← h, ncard_insert_of_notMem hat (hs.subset ((subset_insert a t).trans_eq h))]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid 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', mrange f = f'.mgraph

Tactic:
by
  obtain ⟨f', hf'⟩ := exists_range_eq_graphOn_univ hf₁ hf
  simp only [Set.ext_iff, Set.mem_range, mem_graphOn, mem_univ, true_and, Prod.forall] at hf'
  use
  { toFun := f'
    map_one' := (hf' _ _).1 ⟨1, map_one _⟩
    map_mul' := by
      simp_rw [hf₁.forall]
      rintro g₁ g₂
      exact (hf' _ _).1 ⟨g₁ * g₂, by simp [Prod.ext_iff, (hf' (f _).1 _).1 ⟨_, rfl⟩]⟩ }
  simpa [SetLike.ext_iff] using hf'

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

Goal state before:
pp: case of
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
h : rel x y
a b : M
fa : f a = x
fb : f b = y
⊢ rel (f a) (f b)

Tactic:
rwa [fa, fb]

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✝
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R✝ M₂
inst✝¹¹ : AddCommMonoid M₃
inst✝¹⁰ : Module R✝ M₃
φ : ι✝ → Type i
inst✝⁹ : (i : ι✝) → AddCommMonoid (φ i)
inst✝⁸ : (i : ι✝) → Module R✝ (φ i)
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : SMul R M
inst✝³ : SMul R N
inst✝² : Module S M
inst✝¹ : Module S N
inst✝ : CompatibleSMul M N R S
f : M →ₗ[S] ι → N
r : R
m : M
⊢ f (r • m) = r • f m

Tactic:
ext i; apply ((LinearMap.proj i).comp f).map_smul_of_tower

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
x✝¹ x✝ : R
hb : (fun x ↦ x * a✝) x✝¹ = (fun x ↦ x * a✝) x✝
x : R
hx : a✝ * x = 1
⊢ x✝¹ = x✝

Tactic:
simpa [mul_assoc, hx] using congr_arg (· * x) hb

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
⊢ (proj j ∘ₗ single R φ i) b = 0

Tactic:
rw [proj_comp_single_ne R φ j i, zero_apply]

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
i : ι
hi : i ∈ I
b : φ i
j : ι
hj : j ∈ J
⊢ j ≠ i
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a < b
⊢ insert b (Ioo a b) = Ioc a b

Tactic:
Ioo_insert_right h

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a < b
⊢ Ioc a b = Ioc a b
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ succ b
⊢ ↑(insert (succ b) (Icc a b)) = ↑(Icc a (succ b))

Tactic:
simpa using Set.insert_Icc_right_eq_Icc_succ h

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

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ insert b (Ico a b) = Ico a (b + 1)

Tactic:
simpa [succ_eq_add_one] using insert_Ico_right_eq_Ico_succ_of_not_isMax h hb

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
hab : a < b
f : ℕ → M
ha : a ∉ Ico (a + 1) b
⊢ ∏ k ∈ Ico a b, f k = ∏ x ∈ insert a (Ico (a + 1) b), f x

Tactic:
Finset.insert_Ico_add_one_left_eq_Ico hab

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
hab : a < b
f : ℕ → M
ha : a ∉ Ico (a + 1) b
⊢ ∏ k ∈ Ico a b, f k = ∏ x ∈ Ico a b, f x
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ (∏ x > a, f x) * f a = ∏ x ≥ a, f x

Tactic:
rw [mul_comm, mul_prod_Ioi_eq_prod_Ici]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
r : ℕ
i : ι
⊢ #(Iio i) ≤ r → (partialSups (disjointed f)) i = (partialSups f) i

Tactic:
hi

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
r : ℕ
i : ι
hi : #(Iio i) ≤ r
⊢ (partialSups (disjointed f)) i = (partialSups f) i
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: case refine_2
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n k : ℕ
⊢ (Iio (k + 1)).sup s = s k

Tactic:
· change (Iic k).sup (s ∘ id) = s k
    rw [← apply_sup_eq_sup_comp_of_nonempty hs nonempty_Iic, sup_Iic]

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

Goal state before:
pp: case a
α : Type u_1
M : Type u_3
inst✝⁵ : CommMonoid M
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → M
a b c x✝ : α
a✝ : x✝ ∈ Ico a b
⊢ f (c + x✝) = f (x✝ + c)

Tactic:
rw [add_comm]

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
i : ℕ
⊢ i < m → i ≤ n

Tactic:
hi

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
i : ℕ
hi : i < m
⊢ i ≤ n
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasAntidiagonal A
a : A
p : Multiplicative A × Multiplicative A
⊢ p.1 * p.2 = ofAdd a ↔ toAdd p.1 + toAdd p.2 = a

Tactic:
rw [Multiplicative.ext_iff, toAdd_mul, toAdd_ofAdd]

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

Goal state before:
pp: case refine_1
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ j ≤ k
⊢ k - j + (n - k) = i

pp: case refine_2
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (∃ a, a + j = k ∧ a + (n - k) = i) → i + j = n ∧ j ≤ k

Tactic:
· rw [add_comm, tsub_add_eq_add_tsub h, ← hi.1, add_assoc, Nat.add_sub_of_le hi.2,
      add_tsub_cancel_right]

Goal state after:
case refine_2
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (∃ a, a + j = k ∧ a + (n - k) = i) → i + j = n ∧ j ≤ k
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ a.1 ≤ k) = (fun a ↦ a.2 ≤ k) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
i j a b : ℕ
⊢ b + a = k ∧ a = i ∧ b + (n - k) = j ↔ a + b = k ∧ a = i ∧ b + (n - k) = j

Tactic:
rw [add_comm]

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

Goal state before:
pp: n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ k ≤ a.2) = (fun a ↦ k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
i j a b : ℕ
⊢ b + a = n - k ∧ a = i ∧ b + k = j ↔ a + b = n - k ∧ a = i ∧ b + k = j

Tactic:
rw [add_comm]

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

Goal state before:
pp: α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
x y : α
⊢ y ∣ x ∧ ¬x ∣ y ↔ DvdNotUnit y x

Tactic:
dvd_and_not_dvd_iff

Goal state after:
α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
x y : α
⊢ DvdNotUnit y x ↔ DvdNotUnit y x
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case left
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ 1 ∉ I

pp: case right
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ ∀ (J : Ideal R) (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J

Tactic:
· 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))

Goal state after:
case right
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ ∀ (J : Ideal R) (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝² : Ring R
I : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : Finite ι
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val✝ : Fintype ι
⊢ f x i ∈ I

Tactic:
rw [pi_eq_sum_univ x]

Goal state after:
case intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝² : Ring R
I : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : Finite ι
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val✝ : Fintype ι
⊢ f (∑ i, x i • fun j ↦ if i = j then 1 else 0) i ∈ I
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
x y : ℕ →₀ P
⊢ f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y

Tactic:
let s := x.support ∪ y.support

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
⊢ f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: case mp
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
⊢ ((∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u) → ∃ u ∈ f, P u ∧ Q u

pp: case mpr
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
⊢ (∃ u ∈ f, P u ∧ Q u) → (∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u

Tactic:
· rintro ⟨⟨u, huf, hPu⟩, v, hvf, hQv⟩
    exact
      ⟨u ∩ v, inter_mem huf hvf, hP inter_subset_left hPu, hQ inter_subset_right hQv⟩

Goal state after:
case mpr
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
⊢ (∃ u ∈ f, P u ∧ Q u) → (∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
m : α → Filter β
⊢ (pure a).bind m = m a

Tactic:
by
  simp only [bind, map_pure, join_pure]

Goal state after: