mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u_1}
hc : c ∈ Ici ℵ₀
⊢ ℵ_ (preAleph.symm c - ω) = c

Tactic:
aleph_eq_preAleph,

Goal state after:
c : Cardinal.{u_1}
hc : c ∈ Ici ℵ₀
⊢ preAleph (ω + (preAleph.symm c - ω)) = c
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u_1}
⊢ ℵ_ 1 ≤ c ↔ ℵ₀ < c

Tactic:
← succ_aleph0,

Goal state after:
c : Cardinal.{u_1}
⊢ succ ℵ₀ ≤ c ↔ ℵ₀ < c
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c < ℵ_ 1 ↔ c ≤ ℵ₀

Tactic:
← succ_aleph0,

Goal state after:
c : Cardinal.{u_1}
⊢ c < succ ℵ₀ ↔ c ≤ ℵ₀
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: b o : Ordinal.{u}
hb : 1 < b
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) (b ^ o)
x y : Ordinal.{u}
hx : x < o
hy : y < o
⊢ (fun x1 x2 ↦ x1 + x2) x y < o

Tactic:
have := ho ((opow_lt_opow_iff_right hb).2 hx) ((opow_lt_opow_iff_right hb).2 hy)

Goal state after:
b o : Ordinal.{u}
hb : 1 < b
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) (b ^ o)
x y : Ordinal.{u}
hx : x < o
hy : y < o
this : (fun x1 x2 ↦ x1 * x2) (b ^ x) (b ^ y) < b ^ o
⊢ (fun x1 x2 ↦ x1 + x2) x y < o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case h₂
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a < b ^ log b a * b

Tactic:
← opow_succ

Goal state after:
case h₂
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a < b ^ succ (log b a)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
n : ℕ
⊢ ω_ ↑n ≤ lift.{v, u} o ↔ ω_ ↑n ≤ o

Tactic:
by
  simpa using lift_le (a := ω_ n)

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 * ⟦α⟧ ≤ ⟦α⟧

Tactic:
ih,

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

Goal state before:
pp: case inl
α : Type u
inst✝ : Nonempty α
h✝ : Finite α
⊢ #α ≤ ℵ₀

Tactic:
exact mk_le_aleph0

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

Goal state before:
pp: case mk
α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ #α ≤ #↑(⋃ i, Iio ↑i)

Tactic:
rw [← mk_univ, ← isCofinal_iff_iUnion_Iio_eq_univ.1 hs, iUnion_coe_set]

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

Goal state before:
pp: α : Type u
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ max #α ℵ₀ ^ c

Tactic:
by
  trans #{ t : Set ((ULift.{u} ℕ) ⊕ α) // #t ≤ c }
  · refine ⟨Embedding.subtypeMap ?_ ?_⟩
    · apply Embedding.image
      use Sum.inr
      apply Sum.inr.inj
    intro s hs
    exact mk_image_le.trans hs
  apply (mk_bounded_set_le_of_infinite ((ULift.{u} ℕ) ⊕ α) c).trans
  rw [max_comm, ← add_eq_max] <;> rfl

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
⊢ (finRecOn fun x ↦ ⟦a x⟧) = fun f x ↦ f a

Tactic:
unfold finRecOn
  simp

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Sort u_2
C : ((i : ι) → Trunc (α i)) → Sort u_4
a : (i : ι) → α i
⊢ (finRecOn fun x ↦ ⟦a x⟧) = fun f x ↦ f a

Tactic:
unfold finRecOn
  simp

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
i : ι
φ : ZeroHom (β i) γ
f : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
j : ι
x✝ : j ∈ sf.toFinset
hji : j ≠ i
⊢ (Pi.single i φ j) (f j) = 0

Tactic:
simp [hji]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr.refine_2
ι : 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
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ∑ x ∈ s, ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = ∑ i ∈ s, ↑(μ i)

pp: case mpr.refine_2
ι : 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
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ∀ x ∈ s, x ∉ (DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩).support → ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = 0

Tactic:
· exact Finset.sum_congr rfl fun x hx => by rw [mk_of_mem hx]

Goal state after:
case mpr.refine_2
ι : 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
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ∀ x ∈ s, x ∉ (DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩).support → ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = 0
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
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji ↦ f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji ↦ f ji.fst ji.snd) ⟨y₁, y₂⟩
h_cases : ¬x₁ = y₁
⊢ f x₁ x₂ ∈ ⨆ i ∈ {y₁}, span R (range (f i))

Tactic:
rw [iSup_singleton]

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji ↦ f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji ↦ f ji.fst ji.snd) ⟨y₁, y₂⟩
h_cases : ¬x₁ = y₁
⊢ f x₁ x₂ ∈ span R (range (f y₁))
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
⊢ ⇑(∏ i ∈ s, ψ i) = ∏ i ∈ s, ⇑(ψ i)

Tactic:
by
  induction s using Finset.cons_induction <;> simp [*]

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

Goal state before:
pp: ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
⊢ ⇑(∑ i ∈ s, ψ i) = ∏ i ∈ s, ⇑(ψ i)

Tactic:
by
  induction s using Finset.cons_induction <;> simp [*]

Goal state after:
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✝ : IsScalarTower R S S
t : R
a b : S[M]
⊢ (t • a) • b = t • a • b

Tactic:
ext; simp [coeff_mul, sum_smul_index', Finsupp.smul_sum, smul_mul_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset β
a✝ : α × β
⊢ a✝ ∈ image₂ Prod.mk s t ↔ a✝ ∈ s ×ˢ t

Tactic:
simp [Prod.ext_iff]

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

Goal state before:
pp: case H.inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f g₁ g₂ : R[A]
eq : (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂
ih :
  ∀ s ∈ g₁.coeff.support ∪ g₂.coeff.support,
    ∀ {g₁_1 g₂_1 : R[A]},
      (fun x ↦ f * x) g₁_1 = (fun x ↦ f * x) g₂_1 →
        g₁_1.coeff.support ∪ g₂_1.coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase s → g₁_1 = g₂_1
h : (g₁.coeff.support ∪ g₂.coeff.support).Nonempty
hf : f.coeff.support.Nonempty
⊢ g₁ = g₂

Tactic:
obtain ⟨af, haf, ag, hag, uniq⟩ := UniqueProds.uniqueMul_of_nonempty hf h

Goal state after:
case H.inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f g₁ g₂ : R[A]
eq : (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂
ih :
  ∀ s ∈ g₁.coeff.support ∪ g₂.coeff.support,
    ∀ {g₁_1 g₂_1 : R[A]},
      (fun x ↦ f * x) g₁_1 = (fun x ↦ f * x) g₂_1 →
        g₁_1.coeff.support ∪ g₂_1.coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase s → g₁_1 = g₂_1
h : (g₁.coeff.support ∪ g₂.coeff.support).Nonempty
hf : f.coeff.support.Nonempty
af : A
haf : af ∈ f.coeff.support
ag : A
hag : ag ∈ g₁.coeff.support ∪ g₂.coeff.support
uniq : UniqueMul f.coeff.support (g₁.coeff.support ∪ g₂.coeff.support) af ag
⊢ g₁ = g₂
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
ι : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CommMonoid M
s✝ : Finset ι
m : ι → M
r : ι → R
i : ι
s : Finset ι
hi : i ∉ s
ih : ∏ i ∈ s, single (m i) (r i) = single (∏ i ∈ s, m i) (∏ i ∈ s, r i)
⊢ single (m i) (r i) * ∏ x ∈ s, single (m x) (r x) = single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i)

Tactic:
ih,

Goal state after:
R : Type u_1
M : Type u_4
ι : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CommMonoid M
s✝ : Finset ι
m : ι → M
r : ι → R
i : ι
s : Finset ι
hi : i ∉ s
ih : ∏ i ∈ s, single (m i) (r i) = single (∏ i ∈ s, m i) (∏ i ∈ s, r i)
⊢ single (m i) (r i) * single (∏ i ∈ s, m i) (∏ i ∈ s, r i) = single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i)
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : One α
s : Finset α
a : α
inst✝³ : DecidableEq β
inst✝² : One β
inst✝¹ : FunLike F α β
inst✝ : OneHomClass F α β
f : F
⊢ image (⇑f) 1 = 1

Tactic:
rw [image_one, map_one, singleton_one]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : One α
inst✝ : One β
a✝ : α × β
⊢ a✝ ∈ 1 ×ˢ 1 ↔ a✝ ∈ 1

Tactic:
simp [Prod.ext_iff]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
hs : s.Nonempty
n : ℕ
⊢ (s ^ Int.negSucc n).Nonempty

Tactic:
by simpa using hs.pow

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
s : Set κ
hs : s.Nonempty
a : (i : κ) → π i
⊢ (a ∈ pi s fun x ↦ ⊥) ↔ a ∈ ⊥

Tactic:
by simpa [mem_pi] using! hs

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
n : ℕ
ih : (monomial n) 1 = X ^ n
⊢ (monomial (n + 1)) 1 = X ^ (n + 1)

Tactic:
rw [pow_succ, ← ih, ← monomial_one_one_eq_X, monomial_mul_monomial, mul_one]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
⊢ X ^ n * p * X = p * X ^ (n + 1)

Tactic:
ih,

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
⊢ p * X ^ n * X = p * X ^ (n + 1)
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_2
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
hne : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ≠ 1 ∨ { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ≠ 1
a' b' : G
hu' :
  { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a' * { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b' =
      { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 * { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 →
    { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a' = { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∧
      { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b' = { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0
ha' : a' ∈ A
hb' : b' ∈ B
he : a' * b' = (a0, b0).1 * (a0, b0).2
⊢ a' = (a0, b0).1 ∧ b' = (a0, b0).2

Tactic:
simp_rw [Function.Embedding.coeFn_mk, mul_left_cancel_iff, mul_right_cancel_iff] at hu'

Goal state after:
case refine_2
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
hne : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ≠ 1 ∨ { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ≠ 1
a' b' : G
ha' : a' ∈ A
hb' : b' ∈ B
he : a' * b' = (a0, b0).1 * (a0, b0).2
hu' : a⁻¹ * a' * (b' * b⁻¹) = a⁻¹ * a0 * (b0 * b⁻¹) → a' = a0 ∧ b' = b0
⊢ a' = (a0, b0).1 ∧ b' = (a0, b0).2
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ Subsingleton R → Subsingleton R[X]

Tactic:
intro
    infer_instance

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
c : R
⊢ (C c * X ^ n).support ⊆ {n}

Tactic:
by
  simpa only [C_mul_X_pow_eq_monomial] using support_monomial_subset n c

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: M : Type u_2
inst✝⁷ : AddCommMonoid M
R : Type u_3
S : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : DistribSMul S R
inst✝¹ : SMulCommClass R S M
inst✝ : IsScalarTower S R M
f : End R M
c : Sˣ
⊢ (c • f).invtSubmodule = f.invtSubmodule

Tactic:
by
  apply le_antisymm ?_ (invtSubmodule_le_invtSubmodule_smul f c.1)
  grw [invtSubmodule_le_invtSubmodule_smul (c.1 • f) c⁻¹.1]
  simp [smul_smul]

Goal state after:
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
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R ↥p
hq : q ∈ invtSubmodule (LinearMap.restrict f hp)
⊢ Submodule.map p.subtype q ∈ f.invtSubmodule

Tactic:
rintro - ⟨⟨x, hx⟩, hx', rfl⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R ↥p
hq : q ∈ invtSubmodule (LinearMap.restrict f hp)
x : M
hx : x ∈ p
hx' : ⟨x, hx⟩ ∈ ↑q
⊢ p.subtype ⟨x, hx⟩ ∈ Submodule.comap f (Submodule.map p.subtype 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 : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
⊢ IsCompl p f.ker

Tactic:
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: case left
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
h : IsCompl p q
⊢ (p.subtype.coprod q.subtype).ker = ⊥

Tactic:
ker_coprod_of_disjoint_range,

Goal state after:
case left
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
h : IsCompl p q
⊢ p.subtype.ker.prod q.subtype.ker = ⊥

case left.hd
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
h : IsCompl p q
⊢ Disjoint p.subtype.range q.subtype.range
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_1
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
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ (linearCombination R id).toFun ((lmapDomain R R g) l) ∈ span R (g '' ↑t1)

Tactic:
rw [← Set.image_id (g '' ↑t1), Finsupp.mem_span_image_iff_linearCombination]
    refine ⟨_, ?_, rfl⟩
    have : Inhabited P := ⟨0⟩
    rw [← Finsupp.lmapDomain_supported _ _ g, mem_map]
    refine ⟨l, hl1, ?_⟩
    rfl

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
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
u : ↥p
⊢ (ofIsCompl h φ ψ) ↑u = φ u

Tactic:
simp [ofIsCompl]

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
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
v : ↥q
⊢ (ofIsCompl h φ ψ) ↑v = ψ v

Tactic:
simp [ofIsCompl]

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
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
c : R₁
⊢ ∀ (x : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)), ofIsCompl h (c • x).1 (c • x).2 = (RingHom.id R₁) c • ofIsCompl h x.1 x.2

Tactic:
φ

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
c : R₁
φ : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)
⊢ ofIsCompl h (c • φ).1 (c • φ).2 = (RingHom.id R₁) c • ofIsCompl h φ.1 φ.2
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
⊢ a * ⨆ i, f i = ⨆ i, a * f i

Tactic:
ENat.mul_iSup

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case mp
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
hf : IsProj ⊥ f
⊢ f = 0

pp: case mpr
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hf : IsProj m 0
⊢ m = ⊥

Tactic:
· ext
    simpa using hf.map_mem _

Goal state after:
case mpr
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hf : IsProj m 0
⊢ m = ⊥
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
x : α
⊢ (singleton r x).toList = [x]

Tactic:
simp [toList, singleton]

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
s₁ s₂ : Set α
R : SetRel α α
inst✝ : R.IsSymm
⊢ s₂ ×ˢ s₁ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ Prod.swap ⁻¹' R

Tactic:
← SetRel.inv,

Goal state after:
α : Type u_1
s₁ s₂ : Set α
R : SetRel α α
inst✝ : R.IsSymm
⊢ s₂ ×ˢ s₁ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ R.inv
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case inr.inl
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
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
a b : G
ha : a ∈ A
hb hb0 : b ∈ B
he0 : a0 * b = (A * B).max' ⋯
he : a * b = a0 * b
⊢ a = a0 ∧ b = b

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 ⟨mul_right_cancel he, rfl⟩

Goal state after:
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
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_2.inr.inl
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
this : UniqueMul A B a0 b0
a b : G
ha : a ∈ A
hb hb1 : b ∈ B
he1 : a1 * b = (A * B).min' ⋯
he : a * b = (a1, b).1 * (a1, b).2
⊢ a = (a1, b).1 ∧ b = (a1, b).2

pp: case refine_2.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' ⋯
this : UniqueMul A B a0 b0
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = (a1, b1).1 * (a1, b1).2
hl : b1 < b
⊢ a = (a1, b1).1 ∧ b = (a1, b1).2

Tactic:
· exact ⟨mul_right_cancel he, rfl⟩

Goal state after:
case refine_2.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' ⋯
this : UniqueMul A B a0 b0
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = (a1, b1).1 * (a1, b1).2
hl : b1 < b
⊢ a = (a1, b1).1 ∧ b = (a1, b1).2