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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : SMulWithZero α β
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : MulOneClass β
inst✝² : PosMulMono β
inst✝¹ : MulPosMono β
inst✝ : IsScalarTower α β β
h : Monotone fun x ↦ x • 1
x✝² : α
ha : 0 ≤ x✝²
x✝¹ x✝ : β
hb : x✝¹ ≤ x✝
⊢ x✝² • x✝¹ ≤ x✝² • x✝

Tactic:
have := mul_le_mul_of_nonneg_left hb (by simpa using h ha)

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : SMulWithZero α β
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : MulOneClass β
inst✝² : PosMulMono β
inst✝¹ : MulPosMono β
inst✝ : IsScalarTower α β β
h : Monotone fun x ↦ x • 1
x✝² : α
ha : 0 ≤ x✝²
x✝¹ x✝ : β
hb : x✝¹ ≤ x✝
this : x✝² • 1 * x✝¹ ≤ x✝² • 1 * x✝
⊢ x✝² • x✝¹ ≤ x✝² • x✝
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Semiring α
inst✝⁴ : AddCommGroup β
inst✝³ : Module α β
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
h : ∀ (a : α), 0 ≤ a → ∀ (b : β), 0 ≤ b → 0 ≤ a • b
_a : α
ha : 0 ≤ _a
b₁ b₂ : β
⊢ b₁ ≤ b₂ → _a • b₁ ≤ _a • b₂

Tactic:
by simpa [sub_nonneg, smul_sub] using h _ ha (b₂ - b₁)

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
⊢ a ∈ s ∪ t

Tactic:
wlog h : DirectedOn (· ≤ ·) (d ∩ s) ∧ IsCofinalFor (d ∩ t) (d ∩ s)

Goal state after:
case inr
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
this :
  ∀ {α : Type u_1} {s t : Set α} {D : Set (Set α)} [inst : Preorder α] (hDL : IsLowerSet D) (hs : DirSupClosedOn D s)
    (ht : DirSupClosedOn D t) ⦃d : Set α⦄ (hD : d ∈ D) (hdu : d ⊆ s ∪ t) (hd₀ : d.Nonempty)
    (hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d) ⦃a : α⦄ (ha : IsLUB d a) (hdst : d ∩ s ∪ d ∩ t = d),
    DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ s) ∧ IsCofinalFor (d ∩ t) (d ∩ s) → a ∈ s ∪ t
h : ¬(DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ s) ∧ IsCofinalFor (d ∩ t) (d ∩ s))
⊢ a ∈ s ∪ t

α✝ : Type u_1
s✝ t✝ : Set α✝
D✝ : Set (Set α✝)
inst✝¹ : Preorder α✝
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ s) ∧ IsCofinalFor (d ∩ t) (d ∩ s)
⊢ a ∈ s ∪ t
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
A : Type u_3
inst✝⁴ : Semiring A
inst✝³ : Module R A
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
S : Submodule A M
inst✝ : Module.Finite R A
hS : S.FG
⊢ (Submodule.restrictScalars R S).FG

Tactic:
by
  rw [← Module.Finite.iff_fg] at *
  exact Module.Finite.trans A S

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

Goal state before:
pp: o : Ordinal.{u_4}
⊢ o.pred < o ↔ ¬IsSuccPrelimit o

Tactic:
(pred_le_self o).lt_iff_ne

Goal state after:
o : Ordinal.{u_4}
⊢ o.pred ≠ o ↔ ¬IsSuccPrelimit o
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
hb : IsSuccLimit b
⊢ a + b ≤ c ↔ ∀ d < b, a + d ≤ c

Tactic:
by
  simpa using (lt_add_iff_of_isSuccLimit hb).not

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

Goal state before:
pp: s : Set Ordinal.{u}
hs : ¬BddAbove s
b : Ordinal.{u}
hb : b ∈ s
⊢ ∃ a, enumOrd s a = b

Tactic:
rwa [← range_enumOrd hs] at hb

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

Goal state before:
pp: case inl.inr
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n < 1 ↔ n < b ∨ b ≤ 1

Tactic:
log_lt_iff_lt_pow hb hn,

Goal state after:
case inl.inr
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ n < b ^ 1 ↔ n < b ∨ b ≤ 1
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inr
b m : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < b ∧ 0 ≠ 0
⊢ log b 0 = m ↔ b ^ m ≤ 0 ∧ 0 < b ^ (m + 1)

Tactic:
· simp [@eq_comm _ 0, hm]

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

Goal state before:
pp: a : Ordinal.{u_1}
a0 : a ≠ 0
⊢ 1 - a = 0

Tactic:
Ordinal.sub_eq_zero_iff_le,

Goal state after:
a : Ordinal.{u_1}
a0 : a ≠ 0
⊢ 1 ≤ a
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ x * y + z - x * ((x * y + z) / x) = z % x

Tactic:
mul_add_div,

Goal state after:
case inr
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ x * y + z - x * (y + z / x) = z % x

case inr.b0
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ x ≠ 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
a b : Ordinal.{u_1}
l : IsSuccLimit a
hb : b ≠ 0
e : b = 0
⊢ IsSuccLimit (a ^ b)

pp: case inr.inl
a : Ordinal.{u_1}
l : IsSuccLimit a
b : Ordinal.{u_1}
hb : succ b ≠ 0
⊢ IsSuccLimit (a ^ succ b)

pp: case inr.inr
a b : Ordinal.{u_1}
l : IsSuccLimit a
hb : b ≠ 0
l' : IsSuccLimit b
⊢ IsSuccLimit (a ^ b)

Tactic:
· exact absurd e hb

Goal state after:
case inr.inl
a : Ordinal.{u_1}
l : IsSuccLimit a
b : Ordinal.{u_1}
hb : succ b ≠ 0
⊢ IsSuccLimit (a ^ succ b)

case inr.inr
a b : Ordinal.{u_1}
l : IsSuccLimit a
hb : b ≠ 0
l' : IsSuccLimit b
⊢ IsSuccLimit (a ^ b)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: m n : ℕ
⊢ ↑(m % n) = ↑m % ↑n

Tactic:
rw [← add_left_cancel_iff, div_add_mod, ← natCast_div, ← natCast_mul, ← Nat.cast_add,
    Nat.div_add_mod]

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

Goal state before:
pp: case inr.inr.limit
a b : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
c : Ordinal.{u_1}
l : IsSuccLimit c
IH : ∀ o' < c, a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal.{u_1}
⊢ (∀ a' < c, ((fun x ↦ a ^ x) ∘ fun x ↦ b + x) a' ≤ d) ↔ a ^ b * a ^ c ≤ d

Tactic:
simpa +contextual [IH] using
      (((isNormal_mul_right <| opow_pos b (pos_iff_ne_zero.2 ha.ne')).comp
        (isNormal_opow ha')).le_iff_forall_le l).symm

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

Goal state before:
pp: b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ clog b n ≤ clog c n

Tactic:
rw [clog_le_iff_le_pow (lt_of_lt_of_le hc hb)]
  calc
    n ≤ c ^ clog c n := le_pow_clog hc _
    _ ≤ b ^ clog c n := Nat.pow_le_pow_left hb _

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

Goal state before:
pp: f : Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
n : ℕ
⊢ f^[n] a ≤ ⨆ n, f^[n] a

Tactic:
exact Ordinal.le_iSup (fun n ↦ f^[n] a) n

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

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a + b ≤ b ↔ a * ω ≤ b

Tactic:
rw [← add_eq_right_iff_mul_omega0_le]
  exact (isNormal_add_right a).strictMono.le_apply.ge_iff_eq'

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

Goal state before:
pp: op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
⊢ ¬BddAbove {o | IsPrincipal op o}

Tactic:
by
  rintro ⟨a, ha⟩
  exact ((le_nfp _ _).trans (ha (isPrincipal_nfp_iSup op (succ a)))).not_gt (lt_succ a)

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

Goal state before:
pp: case inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂✝ : o ≠ 2
ho₂ : 2 < o
⊢ ∀ b < o, b * 2 < o

Tactic:
exact fun a ha ↦ ho ha ho₂

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

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

Tactic:
← ord_aleph

Goal state after:
o : Ordinal.{u_1}
⊢ IsSuccLimit (ℵ_ o).ord
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: ι : Type u_1
c : Cardinal.{u_1}
f : ι → Ordinal.{u_1}
hι : #ι ≤ c
hf : ∀ (i : ι), (f i).card ≤ c
⊢ (⨆ i, f i).card ≤ c

Tactic:
by
  rw [← Cardinal.lift_le] at hι
  simpa using card_iSup_le_lift hι hf

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

Goal state before:
pp: a : Ordinal.{u_1}
h : a ≠ 0
⊢ (ω ^ a).card = max ℵ₀ a.card

Tactic:
rw [card_opow_eq_of_omega0_le_left le_rfl h.bot_lt, card_omega0]

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 ≤ ⟦α⟧
⊢ ⟦α⟧ ^ ↑n.succ ≤ ⟦α⟧

Tactic:
grw [Nat.cast_succ, power_add, power_one, ih, mul_eq_self H1]

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

Goal state before:
pp: β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ #↑Set.univ < #?m.36

pp: β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ Type ?u.37

Tactic:
← preimage_univ,

Goal state after:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ #↑(?m.44 ⁻¹' Set.univ) < #?m.42

β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ Type ?u.40

β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ Type ?u.39

β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ ?m.42 → ?m.43
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
inst✝ : Infinite α
⊢ ∃ a, Infinite ↑(f ⁻¹' {a})

Tactic:
suffices Infinite β from exists_infinite_fiber f h

Goal state after:
β α : Type u
f : β → α
h : #α < #β
inst✝ : Infinite α
⊢ Infinite β
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → Zero (δ i j)
inst✝ : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
⊢ (single i (single j x)).sigmaUncurry = single ⟨i, j⟩ x

Tactic:
ext ⟨i', j'⟩

Goal state after:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → Zero (δ i j)
inst✝ : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
i' : ι
j' : α i'
⊢ (single i (single j x)).sigmaUncurry ⟨i', j'⟩ = (single ⟨i, j⟩ x) ⟨i', j'⟩
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: case refine_2
ι : Type u
γ : Type w
inst✝⁵ : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝⁴ : (i : ι) → Zero (β₁ i)
inst✝³ : (i : ι) → Zero (β₂ i)
inst✝² : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
⊢ ∀ x ∈ g.support, h x ((mk g.support fun i ↦ f (↑i) (g ↑i)) x) = (fun i b ↦ h i (f i b)) x (g x)

Tactic:
intro i h1

Goal state after:
case refine_2
ι : Type u
γ : Type w
inst✝⁵ : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝⁴ : (i : ι) → Zero (β₁ i)
inst✝³ : (i : ι) → Zero (β₂ i)
inst✝² : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
i : ι
h1 : i ∈ g.support
⊢ h i ((mk g.support fun i ↦ f (↑i) (g ↑i)) i) = (fun i b ↦ h i (f i b)) i (g i)
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : Function.Injective (mapRange f hf)
i : ι
x y : β₁ i
eq : f i x = f i y
⊢ mapRange f hf (single i x) = mapRange f hf (single i y)

Tactic:
by
    simpa using congr_arg _ eq

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (i : ι), β i
i : ι
⊢ ((fun f ↦ mapRange (fun i ↦ ⇑(Equiv.cast ⋯)) ⋯ (comapDomain' ⇑h ⋯ f)) (comapDomain' ⇑h.symm ⋯ f)) i = f i

Tactic:
mapRange_apply,

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (i : ι), β i
i : ι
⊢ (Equiv.cast ⋯) ((comapDomain' ⇑h ⋯ (comapDomain' ⇑h.symm ⋯ f)) i) = f i
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (k : κ), β (h.symm k)
k : κ
⊢ ((fun f ↦ mapRange (fun i ↦ ⇑(Equiv.cast ⋯)) ⋯ (comapDomain' ⇑h ⋯ f)) f) (h.symm k) = f k

Tactic:
mapRange_apply,

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (k : κ), β (h.symm k)
k : κ
⊢ (Equiv.cast ⋯) ((comapDomain' ⇑h ⋯ f) (h.symm k)) = f k
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsReflexive R M
M' : Type u_6
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ eval R M' ∘ₗ f ∘ₗ ↑(evalEquiv R M).symm = f.dualMap.dualMap

Tactic:
rw [← LinearMap.comp_assoc, LinearEquiv.comp_toLinearMap_symm_eq,
    evalEquiv_toLinearMap, eval_naturality]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : iSupIndep m
⊢ iSupIndep fun i ↦ map f (m i)

Tactic:
simp_rw [iSupIndep, disjoint_iff_inf_le] at ind ⊢

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ j, ⨆ (_ : j ≠ i), m j ≤ ⊥
⊢ ∀ (i : ι), map f (m i) ⊓ ⨆ j, ⨆ (_ : j ≠ i), map f (m j) ≤ ⊥
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case refine_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
u v : R
hu : IsUnit u
hv : IsUnit v
s t : R
hst : s • x + t • y = 0
h : (s * ↑hu.unit⁻¹) • u • x + (t * ↑hv.unit⁻¹) • v • y = 0 → s = 0 ∧ t = 0
⊢ s = 0 ∧ t = 0

Tactic:
apply h

Goal state after:
case refine_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
u v : R
hu : IsUnit u
hv : IsUnit v
s t : R
hst : s • x + t • y = 0
h : (s * ↑hu.unit⁻¹) • u • x + (t * ↑hv.unit⁻¹) • v • y = 0 → s = 0 ∧ t = 0
⊢ (s * ↑hu.unit⁻¹) • u • x + (t * ↑hv.unit⁻¹) • v • y = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case refine_2
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
u v : R
hu : IsUnit u
hv : IsUnit v
s t : R
hst : s • u • x + t • v • y = 0
h : (s * ↑hu.unit) • x + (t * ↑hv.unit) • y = 0 → s = 0 ∧ t = 0
⊢ s = 0 ∧ t = 0

Tactic:
apply h

Goal state after:
case refine_2
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
u v : R
hu : IsUnit u
hv : IsUnit v
s t : R
hst : s • u • x + t • v • y = 0
h : (s * ↑hu.unit) • x + (t * ↑hv.unit) • y = 0 → s = 0 ∧ t = 0
⊢ (s * ↑hu.unit) • x + (t * ↑hv.unit) • y = 0
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
inst✝³ : Semiring S
inst✝² : DistribSMul R S
inst✝¹ : Mul M
inst✝ : SMulCommClass R S S
t : R
a b : S[M]
⊢ t • a • b = a • t • b

Tactic:
ext; simp [coeff_mul, sum_smul_index', Finsupp.smul_sum, mul_smul_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 β
⊢ ↑(image₂ f s t) = ↑(image₂ (fun a b ↦ f b a) t s)

Tactic:
by
    push_cast
    exact image2_swap _ _ _

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq α'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
⊢ ↑(image g (image₂ f s t)) = ↑(image₂ f' (image g' s) t)

Tactic:
push_cast
    exact image_image2_distrib_left h_distrib

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
x : R[N]
hx : ↑x.coeff.support ⊆ Set.range f
hf : Injective f
⊢ mapDomain f (comapDomain f hf x) = x

Tactic:
ext : 1

Goal state after:
R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
x : R[N]
hx : ↑x.coeff.support ⊆ Set.range f
hf : Injective f
⊢ (mapDomain f (comapDomain f hf x)).coeff = x.coeff
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝² : Semiring R
inst✝¹ : Mul M
inst✝ : Mul N
e : M ≃ N
x : R[M]
⊢ ((mapDomainAddEquiv R e) x).coeff = equivMapDomain e x.coeff

Tactic:
by ext; simp [mapDomainAddEquiv]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
r₁ r₂ : R
m : M
⊢ single m r₁ = single m r₂ ↔ r₁ = r₂

Tactic:
simp +contextual [single_inj]

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

Goal state before:
pp: ι : Type u_14
α : ι → Type u_15
β : ι → Type u_16
γ : ι → Type u_17
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → α i → β i → γ i
s : (i : ι) → Finset (α i)
t : (i : ι) → Finset (β i)
⊢ (piFinset fun i ↦ image₂ (f i) (s i) (t i)) = image₂ (fun a b i ↦ f i (a i) (b i)) (piFinset s) (piFinset t)

Tactic:
ext; simp only [mem_piFinset, mem_image₂, Classical.skolem, forall_and, funext_iff]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: case refine_2.inr
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
hnotMem : ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support)
x✝ : True
bg : b0 ∉ g.coeff.support
⊢ f.coeff a0 * g.coeff b0 = 0

Tactic:
notMem_support_iff.mp bg,

Goal state after:
case refine_2.inr
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
hnotMem : ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support)
x✝ : True
bg : b0 ∉ g.coeff.support
⊢ f.coeff a0 * 0 = 0
Module: Mathlib.LinearAlgebra.Finsupp.Span

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
⊢ ⨆ a, (lsingle a).range = ⊤

Tactic:
refine eq_top_iff.2 <| SetLike.le_def.2 fun f _ => ?_
  rw [← sum_single f]
  exact sum_mem fun a _ => Submodule.mem_iSup_of_mem a ⟨_, rfl⟩

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ ((monomial n) a).toFinsupp = single n a

Tactic:
toFinsupp_monomial

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ single n a = single n a
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
⊢ ((monomial 1) a).toFinsupp = single 1 a

Tactic:
toFinsupp_monomial

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
⊢ single 1 a = single 1 a
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ ((monomial n) 1).toFinsupp = single n 1

Tactic:
toFinsupp_monomial

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ single n 1 = single n 1
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
G : Type u_3
inst✝² : Monoid G
inst✝¹ : DistribMulAction G M
inst✝ : SMulCommClass G R M
x : M
g : G
y : M
hy : y ∈ MulAction.orbit G x
⊢ g • y ∈ span R (MulAction.orbit G x)

Tactic:
exact Submodule.subset_span <| MulAction.mem_orbit_of_mem_orbit g hy

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)
⊢ lcomapDomain u hu = LinearMap.linearProjOfIsCompl (span R (Set.range fun x ↦ single (v x) 1)) (lmapDomain R R u) ⋯ ⋯

Tactic:
refine Finsupp.basisSingleOne.ext fun i ↦ ?_

Goal state after:
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 : ι
⊢ (lcomapDomain u hu) (Finsupp.basisSingleOne i) =
    (LinearMap.linearProjOfIsCompl (span R (Set.range fun x ↦ single (v x) 1)) (lmapDomain R R u) ⋯ ⋯)
      (Finsupp.basisSingleOne i)
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inr.inr.coe
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
d : ℕ
h : ∀ (i : ι), a * f i ≤ ↑d
hlt : ⨆ i, f i < ⊤
j : ι
hj : f j = ⨆ i, f i
⊢ a * f j ≤ ↑d

Tactic:
apply h

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : TwoUniqueProds G
inst✝ : TwoUniqueProds H
⊢ TwoUniqueProds (G × H)

Tactic:
have : ∀ b, TwoUniqueProds (I G H b) := Bool.rec ?_ ?_

Goal state after:
case refine_3
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : TwoUniqueProds G
inst✝ : TwoUniqueProds H
⊢ TwoUniqueProds (I G H true)

case refine_1
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : TwoUniqueProds G
inst✝ : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
⊢ TwoUniqueProds (G × H)

case refine_2
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : TwoUniqueProds G
inst✝ : TwoUniqueProds H
⊢ TwoUniqueProds (I G H false)
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case inr.inr
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a0 * b0
hl : b0 < b
⊢ a = a0 ∧ b = b0

Tactic:
· exact ((he0 ▸ mul_lt_mul_right hl a0).not_ge <| le_max' _ _ <| mul_mem_mul ha0 hb).elim

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

Goal state before:
pp: case refine_5
R✝ : Type u_1
M✝ : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
P✝ : Type u_6
P' : Type u_7
inst✝¹³ : Semiring R✝
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : AddCommGroup N✝
inst✝¹⁰ : AddCommGroup P✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module R✝ N✝
inst✝⁷ : Module R✝ P✝
f✝ : M✝ →ₗ[R✝] N✝
g✝ : N✝ →ₗ[R✝] P✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hg : Surjective ⇑g
⊢ RightInverse (fun e ↦ ⟨fst R M P ∘ₗ ↑↑e, ⋯⟩) fun l ↦ ⟨LinearEquiv.ofBijective ((↑l).prod g) ⋯, ⋯⟩

Tactic:
· rintro ⟨e, rfl, rfl⟩
    ext x <;> simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
hi : ↑i + 1 ≤ p.length
⊢ (p.toFun i.succ.rev, p.toFun i.castSucc.rev) ∈ r

Tactic:
convert! p.step ⟨p.length - (i.1 + 1), Nat.sub_lt_self (by lia) hi⟩

Goal state after:
case e'_3
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
hi : ↑i + 1 ≤ p.length
⊢ i.succ.rev = ⟨p.length - (↑i + 1), ⋯⟩.castSucc

case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
hi : ↑i + 1 ≤ p.length
⊢ i.castSucc.rev = ⟨p.length - (↑i + 1), ⋯⟩.succ