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

Goal state before:
pp: a b c : Ordinal.{u_4}
h : a ≤ b * c
⊢ a / b ≤ c

Tactic:
obtain rfl | b0 := eq_or_ne b 0

Goal state after:
case inl
a c : Ordinal.{u_4}
h : a ≤ 0 * c
⊢ a / 0 ≤ c

case inr
a b c : Ordinal.{u_4}
h : a ≤ b * c
b0 : b ≠ 0
⊢ a / b ≤ c
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b x y : ℕ
hy : y ≠ 0
h : x ≤ log b y
hb : b ≤ 1
⊢ b ^ x ≤ y

Tactic:
rw [log_of_left_le_one hb, Nat.le_zero] at h

Goal state after:
b x y : ℕ
hy : y ≠ 0
h : x = 0
hb : b ≤ 1
⊢ b ^ x ≤ y
Module: Mathlib.Data.Nat.Log

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

Tactic:
not_and_or,

Goal state after:
case inr
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : ¬1 < b ∨ ¬n ≠ 0
hm : m ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b : Ordinal.{u_1}
ha : a ≠ 0
hb : IsSuccLimit b
⊢ a ^ b = ⨆ x, a ^ ↑x

Tactic:
simp_rw [opow_of_ne_zero ha, limitRecOn_limit _ _ _ _ hb]

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

Goal state before:
pp: a : Ordinal.{u_1}
h : 1 < a
⊢ IsNormal fun x ↦ a ^ x

Tactic:
have ha : 0 < a := zero_lt_one.trans h
  refine IsNormal.of_succ_lt ?_ fun hl ↦ ?_
  · simpa only [mul_one, opow_succ] using fun b ↦ mul_lt_mul_of_pos_left h (opow_pos b ha)
  · simp [IsLUB, IsLeast, upperBounds, lowerBounds, ← opow_le_of_isSuccLimit ha.ne' hl]

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

Goal state before:
pp: x y z : Ordinal.{u_4}
⊢ x * y % (x * z) = x * (y % z)

Tactic:
obtain rfl | hx := eq_zero_or_pos x

Goal state after:
case inl
y z : Ordinal.{u_4}
⊢ 0 * y % (0 * z) = 0 * (y % z)

case inr
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * y % (x * z) = x * (y % z)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case pos
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : BddAbove s
⊢ o * sSup s = sSup ((fun x ↦ o * x) '' s)

pp: case neg
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ o * sSup s = sSup ((fun x ↦ o * x) '' s)

Tactic:
· exact (isNormal_mul_right ho).map_sSup hs bdd

Goal state after:
case neg
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ o * sSup s = sSup ((fun x ↦ o * x) '' s)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b (n / b * b) = log b n

pp: case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b * b) = log b n

Tactic:
· rw [div_eq_of_lt h, Nat.zero_mul, log_zero_right, log_of_lt h]

Goal state after:
case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b * b) = log b n
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ (n + b).pred.succ ≤ n * b

Tactic:
succ_pred_eq_of_pos (by lia)

Goal state after:
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ n + b ≤ n * b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
rw [← Ordinal.add_sub_cancel_of_le h, ← add_assoc, natCast_add_omega0]

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

Goal state before:
pp: b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
⊢ log b (o % b ^ log b o) < log b o

Tactic:
rcases eq_or_ne (o % (b ^ log b o)) 0 with h | h
  · rw [h, log_zero_right]
    exact log_pos hb (one_le_iff_ne_zero.1 (hb.le.trans hbo)) hbo
  · rw [← lt_opow_iff_log_lt hb h]
    exact mod_lt _ (opow_pos _ hb.pos).ne'

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

Goal state before:
pp: case pos.inl
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
this : IsPrincipal op (sSup ∅)
H : ∀ x ∈ ∅, IsPrincipal op x
hs : BddAbove ∅
⊢ IsPrincipal op (sSup ∅)

pp: case pos.inr
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
hs' : s.Nonempty
⊢ IsPrincipal op (sSup s)

Tactic:
· assumption

Goal state after:
case pos.inr
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
hs' : s.Nonempty
⊢ IsPrincipal op (sSup s)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case mpr
a b : Ordinal.{u_1}
hb : b ≠ 0
⊢ (∃ c < b, ∃ n, a < ω ^ (ω ^ c * ↑n)) → ∃ c, (∃ c_1 < b, ∃ n, c < ω ^ c_1 * ↑n) ∧ ∃ n, a < ω ^ c * ↑n

Tactic:
intro ⟨a, ha, ⟨n, hn⟩⟩
    refine ⟨ω ^ a * n, ⟨a, ha, n + 1, ?_⟩, 1, ?_⟩
    · simp [mul_lt_mul_iff_right₀, opow_pos]
    · simpa

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

Goal state before:
pp: ⊢ ω_ 0 = ω

Tactic:
rw [omega_eq_preOmega, add_zero, preOmega_omega0]

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof = 0 ∨ o.cof = 1 ↔ ¬(o ≠ 0 ∧ IsSuccPrelimit o)

Tactic:
not_and_or,

Goal state after:
o : Ordinal.{u_1}
⊢ o.cof = 0 ∨ o.cof = 1 ↔ ¬o ≠ 0 ∨ ¬IsSuccPrelimit o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b

Tactic:
obtain rfl | b0 := eq_or_ne b 0

Goal state after:
case inl
a : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ 0
⊢ a * ω ^ ω ^ 0 = ω ^ ω ^ 0

case inr
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case isSuccPrelimit
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
⊢ lift.{v, u_1} (preBeth o) = preBeth (Ordinal.lift.{v, u_1} o)

Tactic:
preBeth_limit ho,

Goal state after:
case isSuccPrelimit
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
⊢ lift.{v, u_1} (⨆ a, preBeth ↑a) = preBeth (Ordinal.lift.{v, u_1} o)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_2.refine_1
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this : StrictMono fun i ↦ ⟨f i, ⋯⟩
b : Ordinal.{u}
hb : b ∈ Iio (⨆ i, f i + 1)
i : β
hi : b ≤ f i
⊢ ∃ y ∈ range fun i ↦ ⟨f i, ⋯⟩, ⟨b, hb⟩ ≤ y

Tactic:
exact ⟨_, Set.mem_range_self i, hi⟩

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

Goal state before:
pp: ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : ℵ₀ ≤ c
⊢ Cardinal.lift.{v, u} #ι * ⨆ i, Cardinal.lift.{u, v} (f i).card ≤ Cardinal.lift.{u, v} c * Cardinal.lift.{u, v} c

Tactic:
apply mul_le_mul' hι (ciSup_le' _)

Goal state after:
ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : ℵ₀ ≤ c
⊢ ∀ (i : ι), Cardinal.lift.{u, v} (f i).card ≤ Cardinal.lift.{u, v} c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case e'_4
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ i, lift.{u, v} (f i)
⊢ lift.{u, v} (⨆ i, f i) = max (lift.{v, u} #ι) (⨆ i, lift.{u, v} (f i))

Tactic:
max_eq_right h,

Goal state after:
case e'_4
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ i, lift.{u, v} (f i)
⊢ lift.{u, v} (⨆ i, f i) = ⨆ i, lift.{u, v} (f i)
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case add_one.h'
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ (a ^ b).card ≠ 0

Tactic:
rw [ne_eq, card_eq_zero, opow_eq_zero]

Goal state after:
case add_one.h'
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ ¬(a = 0 ∧ b ≠ 0)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ (prod fun i ↦ lift.{u, v} (c i)) ≤ lift.{v, u} (2 ^ #ι)

Tactic:
refine (prod_le_prod _ _ h₂).trans_eq ?_

Goal state after:
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ (prod fun i ↦ lift.{v, u} #ι) = lift.{v, u} (2 ^ #ι)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case pos
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : (if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 }) = Sum.inl x
h' : ∃ z, g z = y
⊢ x ∈ ↑⟨s, ⋯⟩

pp: case neg
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : (if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 }) = Sum.inl x
h' : ¬∃ z, g z = y
⊢ x ∈ ↑⟨s, ⋯⟩

Tactic:
· rw [dif_pos h'] at h
      cases Sum.inl.inj h
      exact (Classical.choose h').2

Goal state after:
case neg
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : (if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 }) = Sum.inl x
h' : ¬∃ z, g z = y
⊢ x ∈ ↑⟨s, ⋯⟩
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case mpr.inr
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
hi : xi = 0
hj : xj = 0
⊢ single i xi = single j xj

Tactic:
· rw [hi, hj, DFinsupp.single_zero, DFinsupp.single_zero]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : Semiring γ
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → Module γ (β i)
c x : γ
y : Π₀ (i : ι), β i
i : ι
⊢ ((c + x) • y) i = (c • y + x • y) i

Tactic:
simp only [add_apply, smul_apply, add_smul]

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

Goal state before:
pp: ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ f.update i b = single i b + erase i f

Tactic:
ext j
  rcases eq_or_ne i j with (rfl | h)
  · simp
  · simp [h, h.symm]

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

Goal state before:
pp: ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ f.update i b = erase i f + single i b

Tactic:
ext j
  rcases eq_or_ne i j with (rfl | h)
  · simp
  · simp [h, h.symm]

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

Goal state before:
pp: ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
ij : (i : ι) × α i
x : δ ij.fst ij.snd
⊢ (single ij x).sigmaCurry = single ij.fst (single ij.snd x)

Tactic:
obtain ⟨i, j⟩ := ij
  ext i' j'
  dsimp only
  rw [sigmaCurry_apply]
  obtain rfl | hi := eq_or_ne i i'
  · rw [single_eq_same]
    obtain rfl | hj := eq_or_ne j' j
    · rw [single_eq_same, single_eq_same]
    · rw [single_eq_of_ne, single_eq_of_ne hj]
      simpa using hj
  · simp [hi]

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

Goal state before:
pp: case pos
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : i = j
⊢ ((sigmaFinsuppEquivDFinsupp (single ⟨i, a⟩ n)) j) b = ((DFinsupp.single ⟨i, a⟩.fst (single ⟨i, a⟩.snd n)) j) b

Tactic:
subst h
    classical simp [split_apply, Finsupp.single_apply]

Goal state after:
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 : ι) → DecidableEq (β i)
f g : Π₀ (i : ι), β i
x✝ : f.support = g.support ∧ ∀ i ∈ f.support, f i = g i
h₁ : f.support = g.support
h₂ : ∀ i ∈ f.support, f i = g i
i : ι
h : i ∉ f.support
hf : f i = 0
hg : g i = 0
⊢ 0 = g i

Tactic:
hg

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → DecidableEq (β i)
f g : Π₀ (i : ι), β i
x✝ : f.support = g.support ∧ ∀ i ∈ f.support, f i = g i
h₁ : f.support = g.support
h₂ : ∀ i ∈ f.support, f i = g i
i : ι
h : i ∉ f.support
hf : f i = 0
hg : g i = 0
⊢ 0 = 0
Module: Mathlib.Data.Fin.Tuple.Reflection

Goal state before:
pp: α : Type u_1
P : (Fin 0 → α) → Prop
⊢ Exists P ↔ ∃ x, P x

Tactic:
by
    simp only [Exists, Fin.exists_fin_zero_pi, Matrix.vecEmpty]
    rfl

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
s t : R
h' : s • x + t • y = 0
h : Finsupp.single 0 s + Finsupp.single 1 t = 0
⊢ s = 0

Tactic:
simpa using congr($h 0)

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case pos
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
x : Π₀ (i : ι), β₂ i
h : ⇑x ∈ AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mrange (f i)
g : (i : ι) → β₁ i
hg : ∀ (i : ι), (f i) (g i) = x i
i : ι
mem : i ∈ x.support
⊢ (f i) (g ↑⟨i, mem⟩) = x i

Tactic:
hg

Goal state after:
case pos
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
x : Π₀ (i : ι), β₂ i
h : ⇑x ∈ AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mrange (f i)
g : (i : ι) → β₁ i
hg : ∀ (i : ι), (f i) (g i) = x i
i : ι
mem : i ∈ x.support
⊢ x i = x i
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), f i ∈ p i
⊢ (DFinsupp.mk f.support fun i ↦ ⟨f ↑i, ⋯⟩).support = f.support

Tactic:
ext; simp [mk_eq_zero]

Goal state after:
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
p : ι → Submodule R N
x : N
⊢ x ∈ iSup p ↔ ∃ f, (∀ (i : ι), f i ∈ p i) ∧ (f.sum fun _i xi ↦ xi) = x

Tactic:
classical
  rw [mem_iSup_iff_exists_dfinsupp']
  refine ⟨fun ⟨f, hf⟩ ↦ ⟨⟨f.support, fun i ↦ (f i : N), by simp⟩, by simp, hf⟩, ?_⟩
  rintro ⟨f, hf, rfl⟩
  refine ⟨DFinsupp.mk f.support fun i ↦ ⟨f i, hf i⟩, Finset.sum_congr ?_ fun i hi ↦ ?_⟩
  · ext; simp [mk_eq_zero]
  · simp [Finsupp.mem_support_iff.mp hi]

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
M' : Type u_5
P' : Type u_6
inst✝¹⁴ : Semiring R
inst✝¹³ : Semiring S
inst✝¹² : SMul S R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
inst✝⁷ : Module S M
inst✝⁶ : Module S P
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : IsScalarTower S R P
inst✝³ : AddCommMonoid M'
inst✝² : Module S M'
inst✝¹ : AddCommMonoid P'
inst✝ : Module S P'
i : M' →ₗ[S] M
k : P' →ₗ[S] P
hk : Injective ⇑k
f : M →ₗ[R] P
hf : ∀ (m : M'), f (i m) ∈ k.range
m : M'
this : k ((i.restrictScalarsRange k hk f hf) m) = (k ∘ₗ (↑S f ∘ₗ i).codLift k hk hf) m
⊢ (↑S f ∘ₗ i) m = f (i m)

Tactic:
comp_apply,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
M' : Type u_5
P' : Type u_6
inst✝¹⁴ : Semiring R
inst✝¹³ : Semiring S
inst✝¹² : SMul S R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
inst✝⁷ : Module S M
inst✝⁶ : Module S P
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : IsScalarTower S R P
inst✝³ : AddCommMonoid M'
inst✝² : Module S M'
inst✝¹ : AddCommMonoid P'
inst✝ : Module S P'
i : M' →ₗ[S] M
k : P' →ₗ[S] P
hk : Injective ⇑k
f : M →ₗ[R] P
hf : ∀ (m : M'), f (i m) ∈ k.range
m : M'
this : k ((i.restrictScalarsRange k hk f hf) m) = (k ∘ₗ (↑S f ∘ₗ i).codLift k hk hf) m
⊢ (↑S f) (i m) = f (i m)
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
inst✝ : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
this : LinearIndependent R ![(a * d - b * c) • x, (a * d - b * c) • y]
⊢ LinearIndependent R ![x, y]

Tactic:
by
    rwa [pair_smul_iff (sub_ne_zero_of_ne h)] at this

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

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a ↦ f ⋯
i : ι
hi : i ∈ s
⊢ v i ∈ t

Tactic:
obtain ⟨a, rfl⟩ := hi

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a ↦ f ⋯
a : ↑t
⊢ v ((fun a ↦ f ⋯) a) ∈ t
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : R[M] →+ N
h : ∀ (m : M) (r : R), f (single m r) = g (single m r)
this : f.comp coeffAddEquiv.symm.toAddMonoidHom = g.comp coeffAddEquiv.symm.toAddMonoidHom
⊢ f = g

Tactic:
convert congr(($this).comp coeffAddEquiv.toAddMonoidHom)

Goal state after:
case e'_2
R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : R[M] →+ N
h : ∀ (m : M) (r : R), f (single m r) = g (single m r)
this : f.comp coeffAddEquiv.symm.toAddMonoidHom = g.comp coeffAddEquiv.symm.toAddMonoidHom
⊢ f = (f.comp coeffAddEquiv.symm.toAddMonoidHom).comp coeffAddEquiv.toAddMonoidHom

case e'_3
R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : R[M] →+ N
h : ∀ (m : M) (r : R), f (single m r) = g (single m r)
this : f.comp coeffAddEquiv.symm.toAddMonoidHom = g.comp coeffAddEquiv.symm.toAddMonoidHom
⊢ g = (g.comp coeffAddEquiv.symm.toAddMonoidHom).comp coeffAddEquiv.toAddMonoidHom
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_1
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
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hu' : UniqueMul C D ({ toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0) ({ toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0)
hne : ¬a = a0 ∨ ¬b0 = b
⊢ ¬(a0 = a ∧ b0 = b)

Tactic:
not_and_or,

Goal state after:
case refine_1
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
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hu' : UniqueMul C D ({ toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0) ({ toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0)
hne : ¬a = a0 ∨ ¬b0 = b
⊢ ¬a0 = a ∨ ¬b0 = b
Module: Mathlib.Order.Sublattice

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : Lattice α
inst✝² : Lattice β
L : Sublattice α
inst✝¹ : Nonempty α
inst✝ : Nonempty β
M : Sublattice β
⊢ L.prod M = ⊤ ↔ L = ⊤ ∧ M = ⊤

Tactic:
by simpa only [← coe_inj] using! Set.prod_eq_univ

Goal state after:
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 : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
⊢ IsCompl p f.ker

Tactic:
by
  constructor
  · rw [disjoint_iff_inf_le]
    rintro x ⟨hpx, hfx⟩
    rw [SetLike.mem_coe, mem_ker, hf ⟨x, hpx⟩, mk_eq_zero] at hfx
    simp only [hfx, zero_mem]
  · rw [codisjoint_iff_le_sup]
    intro x _
    rw [mem_sup']
    refine ⟨f x, ⟨x - f x, ?_⟩, add_sub_cancel _ _⟩
    rw [mem_ker, map_sub, hf, sub_self]

Goal state after:
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 = x - (p.projection q hpq) x

Tactic:
by
  rw [eq_sub_iff_add_eq, projection_add_projection_eq_self]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝⁴ : Semiring S
M : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_7
inst✝¹ : AddCommMonoid E
inst✝ : Module S E
p : E →ₗ[S] M
⊢ (∀ (x : E), (q ∘ₗ p) x = p x) ↔ p.range ≤ q.range

Tactic:
comp_apply,

Goal state after:
S : Type u_5
inst✝⁴ : Semiring S
M : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_7
inst✝¹ : AddCommMonoid E
inst✝ : Module S E
p : E →ₗ[S] M
⊢ (∀ (x : E), q (p x) = p x) ↔ p.range ≤ q.range
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ height a ≤ n ↔ ∀ ⦃p : LTSeries α⦄, RelSeries.last p = a → ↑p.length ≤ n

Tactic:
constructor
  · rw [height_le_iff]
    exact fun h p hlast => h (le_of_eq hlast)
  · exact height_le

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring 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 : f.range ≤ g.ker
⊢ (∀ (x : N ⧸ f.range), (f.range.liftQ g h) x = 0 ↔ x = 0) → ∀ (x : N), g x = 0 ↔ ∃ y, f y = x

Tactic:
intro hfg x

Goal state after:
case mp
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring 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 : f.range ≤ g.ker
hfg : ∀ (x : N ⧸ f.range), (f.range.liftQ g h) x = 0 ↔ x = 0
x : N
⊢ g x = 0 ↔ ∃ y, f y = x
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring 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 : f.range ≤ g.ker
⊢ (∀ (x : N), g x = 0 ↔ ∃ y, f y = x) → ∀ (x : N ⧸ f.range), (f.range.liftQ g h) x = 0 ↔ x = 0

Tactic:
intro hfg x

Goal state after:
case mpr
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring 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 : f.range ≤ g.ker
hfg : ∀ (x : N), g x = 0 ↔ ∃ y, f y = x
x : N ⧸ f.range
⊢ (f.range.liftQ g h) x = 0 ↔ x = 0
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α) (b : β), f a < b → ∃ a', a < a' ∧ f a' = b
a : α
⊢ coheight a = coheight (f a)

Tactic:
refine le_antisymm (Order.coheight_le_coheight_apply_of_strictMono _ hf _) ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α) (b : β), f a < b → ∃ a', a < a' ∧ f a' = b
a : α
⊢ coheight (f a) ≤ coheight a