mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
l m : List α
o : Ordinal.{u}
hl : l.SortedGT
hm : m.SortedGT
hlt : ∀ i ∈ l, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
hmltl : Lex (fun x1 x2 ↦ x1 < x2) m l
⊢ ∀ i ∈ m, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o

Tactic:
cases l with
  | nil => simp at hmltl
  | cons a as =>
    cases m with
    | nil => intro i hi; simp at hi
    | cons b bs =>
      intro i hi
      suffices h : i ≤ a by refine lt_of_le_of_lt ?_ (hlt a mem_cons_self); simpa
      cases hi with
      | head as => exact List.head_le_of_lt hmltl
      | tail b hi => exact le_of_lt (lt_of_lt_of_le (List.rel_of_pairwise_cons hm.pairwise hi)
          (List.head_le_of_lt hmltl))

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

Goal state before:
pp: b : Bool
n : ℕ
hn : n ≠ 0
⊢ log 2 (n * 2) = log 2 n + 1

Tactic:
log_mul_base Nat.one_lt_two hn

Goal state after:
b : Bool
n : ℕ
hn : n ≠ 0
⊢ log 2 n + 1 = log 2 n + 1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b c : Ordinal.{u_1}
ab : a < b
⊢ a ^ succ c < b ^ succ c

Tactic:
by
  rw [opow_succ, opow_succ]
  exact mul_lt_mul_of_le_of_lt_of_nonneg_of_pos (by gcongr) ab zero_le (opow_pos _ ab.bot_lt)

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b c : Ordinal.{u_1}
h : b ≤ c
⊢ a ^ c = a ^ b * a ^ (c - b)

Tactic:
rw [← opow_add, Ordinal.add_sub_cancel_of_le h]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_4}
h : ω ≤ o
n : ℕ
⊢ ↑n + ω + (o - ω) = ω + (o - ω)

Tactic:
natCast_add_omega0

Goal state after:
o : Ordinal.{u_4}
h : ω ≤ o
n : ℕ
⊢ ω + (o - ω) = ω + (o - ω)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ log b x + log b y ≤ log b (x * y)

Tactic:
rw [← opow_le_iff_le_log hb (mul_ne_zero hx hy), opow_add]

Goal state after:
case inl
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ b ^ log b x * b ^ log b y ≤ x * y
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
m n : ℕ
hm : m ≤ 1
⊢ ↑(Nat.log m n) = log ↑m ↑n

pp: case inr
m n : ℕ
hm : 1 < m
⊢ ↑(Nat.log m n) = log ↑m ↑n

Tactic:
case inl => rw_mod_cast [Nat.log_of_left_le_one hm, log_of_left_le_one (mod_cast hm)]

Goal state after:
case inr
m n : ℕ
hm : 1 < m
⊢ ↑(Nat.log m n) = log ↑m ↑n
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: a b : Ordinal.{u_1}
ha : a.IsInitial
⊢ a.card ≤ b.card ↔ a ≤ b

Tactic:
by
  refine ⟨fun h ↦ ?_, Ordinal.card_le_card⟩
  rw [← ha.le_ord_iff_card_le] at h
  grw [h, ord_card_le]

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

Goal state before:
pp: n : ℕ
⊢ preAleph ↑n = ↑n

Tactic:
rw [← card_preOmega, preOmega_natCast, card_nat]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (a * b)

Tactic:
by
  rcases eq_zero_or_pos a with (rfl | _)
  · rw [zero_mul]
    exact isPrincipal_zero
  · rcases eq_zero_or_pos b with (rfl | hb₁')
    · rw [mul_zero]
      exact isPrincipal_zero
    · rw [← one_le_iff_pos] at hb₁'
      intro c d hc hd
      rw [lt_mul_iff_of_isSuccLimit
        (isSuccLimit_of_isPrincipal_add (lt_of_le_of_ne hb₁' hb₁.symm) hb)] at *
      rcases hc with ⟨x, hx, hx'⟩
      rcases hd with ⟨y, hy, hy'⟩
      use x + y, hb hx hy
      rw [mul_add]
      exact Left.add_lt_add hx' hy'

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ IsSuccLimit (ℵ_ o).ord

Tactic:
exact isSuccLimit_ord (aleph0_le_aleph _)

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_2
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 ↦ x1 * x2) a b < o

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)
    · dsimp only; rwa [zero_mul]
    rw [← pos_iff_ne_zero] at ha
    rw [← h a ha hao]
    exact (isNormal_mul_right ha).strictMono hbo

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr.inr
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
⊢ a * b < ω ^ c

Tactic:
rcases ((isNormal_opow one_lt_omega0).lt_iff_exists_lt l).1 ha with ⟨x, hx, ax⟩

Goal state after:
case inr.inr
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
⊢ a * b < ω ^ c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ b ≤ a + b

Tactic:
apply self_le_add_left

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

Goal state before:
pp: case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
hb : b < c
this : a + b < c
⊢ False

Tactic:
simp [h] at this

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: a o : Ordinal.{u_1}
ha : o.cof.ord = a
⊢ ∃ f, IsFundamentalSeq f

Tactic:
by
  subst ha
  obtain ⟨s, hs, hs'⟩ := exists_ord_cof_eq o.ToType
  rw [cof_toType] at hs'
  let g := (OrderIso.setCongr _ _ (congrArg _ hs'.symm)).trans <|
    .ofRelIsoLT (enum (α := s) (· < ·))
  refine ⟨fun i ↦ g i, le_rfl, fun _ ↦ by simp, ?_⟩
  rw [range_comp', OrderIso.map_isCofinal_iff, range_comp', g.range_eq]
  simpa

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

Goal state before:
pp: κ μ : Cardinal.{u}
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n✝ : ℕ
H3 : μ = ↑n✝
α : Type u
H1 : ℵ₀ ≤ ⟦α⟧
n : ℕ
ih : ⟦α⟧ ^ ↑n ≤ ⟦α⟧
⊢ ⟦α⟧ * ⟦α⟧ ≤ ⟦α⟧

Tactic:
mul_eq_self H1

Goal state after:
κ μ : Cardinal.{u}
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n✝ : ℕ
H3 : μ = ↑n✝
α : Type u
H1 : ℵ₀ ≤ ⟦α⟧
n : ℕ
ih : ⟦α⟧ ^ ↑n ≤ ⟦α⟧
⊢ ⟦α⟧ ≤ ⟦α⟧
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c < ℵ₀ ∨ c.IsRegular ∨ c.IsSingular

Tactic:
have := isRegular_or_isSingular (c := c)

Goal state after:
c : Cardinal.{u_1}
this : ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
⊢ c < ℵ₀ ∨ c.IsRegular ∨ c.IsSingular
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
s : Finset α
⊢ #↑(↑s)ᶜ = #α

Tactic:
by
  apply mk_compl_of_infinite
  exact (finset_card_lt_aleph0 s).trans_le (aleph0_le_mk α)

Goal state after:
Module: Mathlib.Data.DFinsupp.Module

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
r : γ
f : Π₀ (i : ι), β i
i✝ : κ
⊢ r • f (h i✝) = r • (comapDomain' h hh' f) i✝

Tactic:
comapDomain'_apply

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
r : γ
f : Π₀ (i : ι), β i
i✝ : κ
⊢ r • f (h i✝) = r • f (h i✝)
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β i) → Decidable (x = 0)
f : Π₀ (i : ι), β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
⊢ (∀ i ∈ ↑s, f i = 0) → f = 0

Tactic:
intro hs₁

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β i) → Decidable (x = 0)
f : Π₀ (i : ι), β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
hs₁ : ∀ i ∈ ↑s, f i = 0
⊢ f = 0
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this✝ : DecidableEq ι
this : (i : ι) → DecidableEq (η i →₀ N)
g : (i : ι) × η i
hg : ¬(f g.fst) g.snd = 0
h : f g.fst = 0
⊢ False

Tactic:
rw [h] at hg

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this✝ : DecidableEq ι
this : (i : ι) → DecidableEq (η i →₀ N)
g : (i : ι) × η i
hg : ¬0 g.snd = 0
h : f g.fst = 0
⊢ False
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd
⊢ f.sigmaCurry.sigmaUncurry = f

Tactic:
by
    ext ⟨i, j⟩
    rw [sigmaUncurry_apply, sigmaCurry_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F G : (i : ι) → M i →ₗ[R] N
⊢ { toFun := ⇑(sumAddHom fun i ↦ ((F + G) i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := ⇑(sumAddHom fun i ↦ (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := ⇑(sumAddHom fun i ↦ (G i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
refine DFinsupp.lhom_ext' (fun i ↦ ?_)

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F G : (i : ι) → M i →ₗ[R] N
i : ι
⊢ { toFun := ⇑(sumAddHom fun i ↦ ((F + G) i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ lsingle i =
    ({ toFun := ⇑(sumAddHom fun i ↦ (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := ⇑(sumAddHom fun i ↦ (G i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }) ∘ₗ
      lsingle i
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
c : S
F : (i : ι) → M i →ₗ[R] N
⊢ { toFun := ⇑(sumAddHom fun i ↦ ((c • F) i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id S) c • { toFun := ⇑(sumAddHom fun i ↦ (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
refine DFinsupp.lhom_ext' (fun i ↦ ?_)

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
c : S
F : (i : ι) → M i →ₗ[R] N
i : ι
⊢ { toFun := ⇑(sumAddHom fun i ↦ ((c • F) i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ lsingle i =
    ((RingHom.id S) c • { toFun := ⇑(sumAddHom fun i ↦ (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }) ∘ₗ
      lsingle i
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (Π₀ (i : ι), M i) →ₗ[R] N
⊢ (fun F ↦ { toFun := ⇑(sumAddHom fun i ↦ (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ })
      ((fun F i ↦ F ∘ₗ lsingle i) F) =
    F

Tactic:
refine DFinsupp.lhom_ext' (fun i ↦ ?_)

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (Π₀ (i : ι), M i) →ₗ[R] N
i : ι
⊢ (fun F ↦ { toFun := ⇑(sumAddHom fun i ↦ (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ })
        ((fun F i ↦ F ∘ₗ lsingle i) F) ∘ₗ
      lsingle i =
    F ∘ₗ lsingle i
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
⊢ a ∈ ⨆ i ∈ s, p i ↔ ∃ μ, ∑ i ∈ s, ↑(μ i) = a

Tactic:
classical
    rw [Submodule.mem_iSup_iff_exists_dfinsupp']
    constructor <;> rintro ⟨μ, hμ⟩
    · use fun i => ⟨μ i, (iSup_const_le : _ ≤ p i) (coe_mem <| μ i)⟩
      rw [← hμ]
      symm
      apply Finset.sum_subset
      · intro x
        contrapose
        intro hx
        rw [mem_support_iff, not_ne_iff]
        ext
        rw [coe_zero, ← mem_bot R]
        suffices ⊥ = ⨆ (_ : x ∈ s), p x from this.symm ▸ coe_mem (μ x)
        exact (iSup_neg hx).symm
      · intro x _ hx
        rw [mem_support_iff, not_ne_iff] at hx
        rw [hx]
        rfl
    · refine ⟨DFinsupp.mk s ?_, ?_⟩
      · rintro ⟨i, hi⟩
        refine ⟨μ i, ?_⟩
        rw [iSup_pos]
        · exact coe_mem _
        · exact hi
      simp only [DFinsupp.sum]
      rw [Finset.sum_subset support_mk_subset, ← hμ]
      · exact Finset.sum_congr rfl fun x hx => by rw [mk_of_mem hx]
      · intro x _ hx
        rw [mem_support_iff, not_ne_iff] at hx
        rw [hx]
        rfl

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ a • d • t = -(a • b • s)

Tactic:
by rw [eq_neg_iff_add_eq_zero, ← smul_add, add_comm, h₂, smul_zero]

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

Goal state before:
pp: case right
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ a • b • s + b • c • t = 0

Tactic:
smul_comm a b,

Goal state after:
case right
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ b • a • s + b • c • t = 0
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
δ : Type u_7
δ' : Type u_8
ε : Type u_9
inst✝² : DecidableEq δ'
inst✝¹ : DecidableEq ε
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ ↑(image₂ f s (image₂ g t u)) = ↑(image₂ g' t (image₂ f' s u))

Tactic:
push_cast
    exact image2_left_comm h_left_comm

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ b ∈ t, Injective fun a ↦ f a b
ht : ((fun b ↦ image (fun a ↦ f a b) s) '' ↑t).PairwiseDisjoint id
⊢ #s ∣ #(image₂ f s t)

Tactic:
rw [← image₂_swap]; exact card_dvd_card_image₂_right hf ht

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
x : α
hx : x ∈ image f univ
⊢ x ∈ s

Tactic:
rcases mem_image.1 hx with ⟨x, _, rfl⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
x : Fin k
left✝ : x ∈ univ
hx : f x ∈ image f univ
⊢ f x ∈ s
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
a b : R[ℕ]
⊢ { toFinsupp := a - b } = { toFinsupp := a } - { toFinsupp := b }

Tactic:
rw [sub_eq_add_neg]

Goal state after:
R : Type u
inst✝ : Ring R
a b : R[ℕ]
⊢ { toFinsupp := a + -b } = { toFinsupp := a } - { toFinsupp := b }
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
a b : R[X]
⊢ (a - b).toFinsupp = a.toFinsupp - b.toFinsupp

Tactic:
rw [sub_eq_add_neg]

Goal state after:
R : Type u
inst✝ : Ring R
a b : R[X]
⊢ (a - b).toFinsupp = a.toFinsupp + -b.toFinsupp
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
this : ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
by
      simp_rw [mem_product]
      obtain ⟨c, hc, d, hd, hne, hu'⟩ := this
      obtain ⟨a0, ha0, rfl⟩ := mem_map.mp hc
      obtain ⟨b0, hb0, rfl⟩ := mem_map.mp hd
      refine ⟨(_, _), ⟨ha0, hb0⟩, (a, b), ⟨ha, hb⟩, ?_, fun a' b' ha' hb' he => ?_, hu⟩
      · simp_rw [Function.Embedding.coeFn_mk, Ne, inv_mul_eq_one, mul_inv_eq_one] at hne
        rwa [Ne, Prod.mk_inj, not_and_or, eq_comm]
      specialize hu' (mem_map_of_mem _ ha') (mem_map_of_mem _ hb')
      simp_rw [Function.Embedding.coeFn_mk, mul_left_cancel_iff, mul_right_cancel_iff] at hu'
      rw [mul_assoc, ← mul_assoc a', he, mul_assoc, mul_assoc] at hu'
      exact hu' rfl

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.coeff n ≠ 0
⊢ ∃ a, ¬p.coeff a = 0 ∧ p.coeff a = p.coeff n

Tactic:
exact ⟨n, h, rfl⟩

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

Goal state before:
pp: R : Type u_1
ι : Type u_3
inst✝ : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : ι
⊢ i ∈ Set.range u ⊔ Set.range v

Tactic:
by rw [codisjoint_iff.mp h.2]; trivial

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Cardinality

Goal state before:
pp: M : Type u_3
inst✝ : AddCommMonoid M
S : AddSubmonoid M
⊢ S.FG ↔ ∃ n f, AddMonoidHom.mrange f = S

Tactic:
by
  rw [← S.toNatSubmodule_toAddSubmonoid, ← Submodule.fg_iff_addSubmonoid_fg,
    Submodule.fg_iff_exists_fin_linearMap]
  exact exists_congr fun n => ⟨fun ⟨f, hf⟩ => ⟨f, hf ▸ LinearMap.range_toAddSubmonoid _⟩,
    fun ⟨f, hf⟩ => ⟨f.toNatLinearMap, Submodule.toAddSubmonoid_inj.mp <|
      hf ▸ LinearMap.range_toAddSubmonoid _⟩⟩

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
⊢ span R ↑(Finset.image g t1 ∪ t2) = s

Tactic:
Finset.coe_union,

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
⊢ span R (↑(Finset.image g t1) ∪ ↑t2) = s
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).1 = 0 ↔ (p.prodEquivOfIsCompl q h) ((p.prodEquivOfIsCompl q h).symm x) ∈ q

Tactic:
coe_prodEquivOfIsCompl',

Goal state after:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).1 = 0 ↔
    ↑((p.prodEquivOfIsCompl q h).symm x).1 + ↑((p.prodEquivOfIsCompl q h).symm x).2 ∈ q
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).2 = 0 ↔ (p.prodEquivOfIsCompl q h) ((p.prodEquivOfIsCompl q h).symm x) ∈ p

Tactic:
coe_prodEquivOfIsCompl',

Goal state after:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).2 = 0 ↔
    ↑((p.prodEquivOfIsCompl q h).symm x).1 + ↑((p.prodEquivOfIsCompl q h).symm x).2 ∈ p
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
hpq : IsCompl p q
x : E
⊢ (q.projection p ⋯) x + (p.projection q hpq) x = x

Tactic:
projection_add_projection_eq_self

Goal state after:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
hpq : IsCompl p q
x : E
⊢ x = x
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝¹² : Ring R
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module R E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R F
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
φ : E →ₗ[R₁] F
x : E
a : ↥p
b : ↥q
hab : ↑a + ↑b = x
right✝ : ∀ (r : ↥p) (s : ↥q), ↑r + ↑s = x → r = a ∧ s = b
⊢ ((ofIsComplProd h).toFun ((fun φ ↦ (φ.domRestrict p, φ.domRestrict q)) φ)) x = φ x

Tactic:
rw [← hab]

Goal state after:
R : Type u_1
inst✝¹² : Ring R
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module R E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R F
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
φ : E →ₗ[R₁] F
x : E
a : ↥p
b : ↥q
hab : ↑a + ↑b = x
right✝ : ∀ (r : ↥p) (s : ↥q), ↑r + ↑s = x → r = a ∧ s = b
⊢ ((ofIsComplProd h).toFun ((fun φ ↦ (φ.domRestrict p, φ.domRestrict q)) φ)) (↑a + ↑b) = φ (↑a + ↑b)