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

Goal state before:
pp: case hab
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ κ₁ < ?inl.refine_1.b

Tactic:
assumption

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

Goal state before:
pp: case inl.refine_1.hbc
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ κ₂ ≤ κ₂ + μ₂

Tactic:
assumption

Goal state after:
case inl.refine_1.hbc
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ κ₂ ≤ κ₂ + μ₂
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case hab
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ μ₁ < ?inl.refine_2.b

Tactic:
assumption

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

Goal state before:
pp: case inl.refine_2.hbc
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ μ₂ ≤ κ₂ + μ₂

Tactic:
assumption

Goal state after:
case inl.refine_2.hbc
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ μ₂ ≤ κ₂ + μ₂
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
ha : ω ≤ a
⊢ (a ^ b).card ≤ max ℵ₀ (max a.card b.card)

Tactic:
· exact (card_opow_le_of_omega0_le_left ha _).trans (le_max_right _ _)

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.ord.cof
hf : ∀ (i : ι), f i < c
⊢ iSup f < c

Tactic:
by
  apply lift_iSup_lt_of_lt_cof_ord _ hf
  rwa [Cardinal.lift_umax, c.lift_id']

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

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
hα : #α < ℵ₀
⊢ #α < ℵ₀.ord.cof

Tactic:
isRegular_aleph0.cof_ord

Goal state after:
β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
hα : #α < ℵ₀
⊢ #α < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
inst✝ : Infinite β
hα : #α < ℵ₀
⊢ #α < ℵ₀.ord.cof

Tactic:
isRegular_aleph0.cof_ord

Goal state after:
β α : Type u
f : β → α
h : #α < #β
inst✝ : Infinite β
hα : #α < ℵ₀
⊢ #α < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
hα : #α < ℵ₀
⊢ #α < (ℵ_ 1).ord.cof

Tactic:
rw [isRegular_aleph_one.cof_ord]; exact hα.trans aleph0_lt_aleph_one

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

Goal state before:
pp: α : Type u
inst✝ : Infinite α
⊢ #(Perm α) = 2 ^ #α

Tactic:
mk_perm_eq_self_power,

Goal state after:
α : Type u
inst✝ : Infinite α
⊢ #α ^ #α = 2 ^ #α
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = #(α → β')
⊢ #(α ≃ α) = #(α → α)

Tactic:
mk_perm_eq_self_power,

Goal state after:
α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = #(α → β')
⊢ #α ^ #α = #(α → α)
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case zero
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
⊢ 0 < c.ord → derivFamily f 0 < c.ord

Tactic:
rw [derivFamily_zero]

Goal state after:
case zero
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
⊢ 0 < c.ord → nfpFamily f 0 < c.ord
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, ⋯⟩

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

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

Goal state before:
pp: case inj'.refine_1
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t ⊆ s

Tactic:
assumption

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

Goal state before:
pp: case inj'.refine_2
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t' ⊆ s

Tactic:
assumption

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Nontrivial R
inst✝¹ : Module R M
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : i.Maximal
Φ : κ → Finset ι := fun k ↦ (b.repr (v k)).support
⊢ Cardinal.lift.{w', w} #ι ≤ Cardinal.lift.{w, w'} #κ

Tactic:
have w₁ : #ι ≤ #(Set.range Φ) := by
    apply Cardinal.le_range_of_union_finset_eq_univ
    exact union_support_maximal_linearIndependent_eq_range_basis b v i m

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Nontrivial R
inst✝¹ : Module R M
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : i.Maximal
Φ : κ → Finset ι := fun k ↦ (b.repr (v k)).support
w₁ : #ι ≤ #↑(range Φ)
⊢ Cardinal.lift.{w', w} #ι ≤ Cardinal.lift.{w, w'} #κ
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i i✝ : ι
⊢ (filter (fun x ↦ i = x) f) i✝ = (single i (f i)) i✝

Tactic:
rw [filter_apply, single_apply]

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i i✝ : ι
⊢ (if i = i✝ then f i✝ else 0) = if h : i = i✝ then Eq.recOn h (f i) else 0
Module: Mathlib.Data.DFinsupp.Module

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
δ : Type u_1
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → SMulZeroClass γ (β i)
inst✝¹ : (i : ι) → SMulZeroClass δ (β i)
inst✝ : ∀ (i : ι), SMulCommClass γ δ (β i)
r : γ
s : δ
m : Π₀ (i : ι), β i
i : ι
⊢ (r • s • m) i = (s • r • m) i

Tactic:
simp only [smul_apply, smul_comm r s (m i)]

Goal state after:
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:
ext ⟨i, j⟩

Goal state after:
ι : 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
i : ι
j : α i
⊢ f.sigmaCurry.sigmaUncurry ⟨i, j⟩ = f ⟨i, j⟩
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst✝ : Decidable (b = 0)
j : ι
⊢ j ∈ (f.update i b).support ↔ j ∈ if b = 0 then (erase i f).support else insert i f.support

Tactic:
split_ifs with hb

Goal state after:
case pos
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst✝ : Decidable (b = 0)
j : ι
hb : b = 0
⊢ j ∈ (f.update i b).support ↔ j ∈ (erase i f).support

case neg
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst✝ : Decidable (b = 0)
j : ι
hb : ¬b = 0
⊢ j ∈ (f.update i b).support ↔ j ∈ insert i f.support
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
⊢ extendWith 0 (single i x) = single (some i) x

Tactic:
ext (_ | j)

Goal state after:
case none
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
⊢ (extendWith 0 (single i x)) none = (single (some i) x) none

case some
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
⊢ (extendWith 0 (single i x)) (some j) = (single (some i) x) (some j)
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
x : α none
⊢ extendWith x 0 = single none x

Tactic:
ext (_ | j)

Goal state after:
case none
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
x : α none
⊢ (extendWith x 0) none = (single none x) none

case some
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
x : α none
j : ι
⊢ (extendWith x 0) (some j) = (single none x) (some j)
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
hf' : ∀ (i : ι) (x y : β₁ i), f i (x + y) = f i x + f i y
g₁ g₂ : Π₀ (i : ι), β₁ i
⊢ mapRange f hf (g₁ + g₂) = mapRange f hf g₁ + mapRange f hf g₂

Tactic:
ext
  simp only [mapRange_apply f, coe_add, Pi.add_apply, hf']

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst✝²⁹ : Semiring R
inst✝²⁸ : Semiring R₂
inst✝²⁷ : Semiring S
inst✝²⁶ : Semiring S₂
M : Type u_5
M₂ : Type u_6
N : Type u_7
N₂ : Type u_8
P : Type u_9
P₂ : Type u_10
Pₗ : Type u_11
inst✝²⁵ : AddCommMonoid M
inst✝²⁴ : AddCommMonoid M₂
inst✝²³ : AddCommMonoid N
inst✝²² : AddCommMonoid N₂
inst✝²¹ : AddCommMonoid P
inst✝²⁰ : AddCommMonoid P₂
inst✝¹⁹ : AddCommMonoid Pₗ
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module R M₂
inst✝¹⁶ : Module S N
inst✝¹⁵ : Module S N₂
inst✝¹⁴ : Module R₂ P
inst✝¹³ : Module S₂ P
inst✝¹² : Module R P₂
inst✝¹¹ : Module S₂ P₂
inst✝¹⁰ : Module R Pₗ
inst✝⁹ : Module S Pₗ
M' : Type u_12
P' : Type u_13
inst✝⁸ : AddCommGroup M'
inst✝⁷ : AddCommGroup P'
inst✝⁶ : Module R M'
inst✝⁵ : Module R₂ P'
inst✝⁴ : Module S₂ P'
inst✝³ : SMulCommClass S₂ R₂ P
inst✝² : SMulCommClass S R Pₗ
inst✝¹ : SMulCommClass S₂ R₂ P'
inst✝ : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
q : Submodule S N
m₁ m₂ : M
x✝ : ↥q
⊢ ((f (m₁ + m₂)).domRestrict q) x✝ = ((f m₁).domRestrict q + (f m₂).domRestrict q) x✝

Tactic:
simp only [map_add, domRestrict_apply, add_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: case mp
R₁ : Type u_3
R₂ : Type u_4
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst✝¹¹ : AddCommMonoid Mₗ
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid Pₗ
inst✝⁸ : AddCommMonoid Qₗ
inst✝⁷ : AddCommMonoid Qₗ'
inst✝⁶ : Module R₁ Mₗ
inst✝⁵ : Module R₂ N
inst✝⁴ : Module R₂ Pₗ
inst✝³ : Module R₁ Pₗ
inst✝² : Module R₁ Qₗ
inst✝¹ : Module R₂ Qₗ'
inst✝ : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
⊢ f₁ = f₂

pp: case mpr
R₁ : Type u_3
R₂ : Type u_4
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst✝¹¹ : AddCommMonoid Mₗ
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid Pₗ
inst✝⁸ : AddCommMonoid Qₗ
inst✝⁷ : AddCommMonoid Qₗ'
inst✝⁶ : Module R₁ Mₗ
inst✝⁵ : Module R₂ N
inst✝⁴ : Module R₂ Pₗ
inst✝³ : Module R₁ Pₗ
inst✝² : Module R₁ Qₗ
inst✝¹ : Module R₂ Qₗ'
inst✝ : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁ = f₂
⊢ f₁.compl₁₂ g g' = f₂.compl₁₂ g g'

Tactic:
· -- B₁.comp l r = B₂.comp l r → B₁ = B₂
    ext x y
    obtain ⟨x', rfl⟩ := hₗ x
    obtain ⟨y', rfl⟩ := hᵣ y
    convert! LinearMap.congr_fun₂ h x' y' using 0

Goal state after:
case mpr
R₁ : Type u_3
R₂ : Type u_4
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst✝¹¹ : AddCommMonoid Mₗ
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid Pₗ
inst✝⁸ : AddCommMonoid Qₗ
inst✝⁷ : AddCommMonoid Qₗ'
inst✝⁶ : Module R₁ Mₗ
inst✝⁵ : Module R₂ N
inst✝⁴ : Module R₂ Pₗ
inst✝³ : Module R₁ Pₗ
inst✝² : Module R₁ Qₗ
inst✝¹ : Module R₂ Qₗ'
inst✝ : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁ = f₂
⊢ f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
Module: Mathlib.Algebra.Algebra.Pi

Goal state before:
pp: α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → Semiring (A₁ i)
inst✝⁴ : (i : ι) → Semiring (A₂ i)
inst✝³ : (i : ι) → Semiring (A₃ i)
inst✝² : (i : ι) → Algebra R (A₁ i)
inst✝¹ : (i : ι) → Algebra R (A₂ i)
inst✝ : (i : ι) → Algebra R (A₃ i)
e : (i : ι) → A₁ i ≃ₐ[R] A₂ i
r : R
⊢ (fun j ↦ (e j) ((algebraMap R ((i : ι) → A₁ i)) r j)) = (algebraMap R ((i : ι) → A₂ i)) r

Tactic:
ext i
      simp

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
N : Type u_6
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : span R (Set.range v) = ⊤
hli : LinearIndependent R (⇑f ∘ v)
⊢ Injective ⇑f

Tactic:
refine (injective_iff_map_eq_zero _).mpr fun x hx ↦ ?_
  have : x ∈ Submodule.span R (.range v) := by rw [hv]; exact mem_top
  obtain ⟨c, rfl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp this
  simp only [map_finsuppSum, map_smul] at hx
  obtain rfl := linearIndependent_iff.mp hli c hx
  simp

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

Goal state before:
pp: A : Type u_1
M : Type u_3
N : Type u_4
inst✝² : AddMonoid A
inst✝¹ : Monoid M
inst✝ : Monoid N
ψ : AddChar A M
hψ : Surjective ⇑ψ
f g : M →* N
h : ⇑((fun f ↦ f.compAddChar ψ) f) = ⇑((fun f ↦ f.compAddChar ψ) g)
⊢ ⇑f = ⇑g

Tactic:
exact hψ.injective_comp_right h

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

Goal state before:
pp: case h.mpr
α : Type u_1
inst✝ : Monoid α
n : ℕ
fi : Fin n → (s : Set α) × ↑s
⊢ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = (List.ofFn ((fun x ↦ ↑x.snd) ∘ fi)).prod

Tactic:
exact ⟨fun i ↦ _, rfl⟩

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

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K ↑t)
⊢ ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = t.card

Tactic:
classical
  have :
    ∀ t : Finset V,
      ∀ s' : Finset V,
        ↑s' ⊆ s →
          s ∩ ↑t = ∅ →
            s ⊆ (span K ↑(s' ∪ t) : Submodule K V) →
              ∃ t' : Finset V, ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card :=
    fun t =>
    Finset.induction_on t
      (fun s' hs' _ hss' =>
        have : s = ↑s' := eq_of_linearIndepOn_id_of_span_subtype hs hs' <| by simpa using hss'
        ⟨s', by simp [this]⟩)
      fun b₁ t hb₁t ih s' hs' hst hss' =>
      have hb₁s : b₁ ∉ s := fun h => by
        have : b₁ ∈ s ∩ ↑(insert b₁ t) := ⟨h, Finset.mem_insert_self _ _⟩
        rwa [hst] at this
      have hb₁s' : b₁ ∉ s' := fun h => hb₁s <| hs' h
      have hst : s ∩ ↑t = ∅ :=
        eq_empty_of_subset_empty <|
          -- Porting note: `-subset_inter_iff` required.
          Subset.trans
            (by simp [inter_subset_inter, -subset_inter_iff])
            (le_of_eq hst)
      Classical.by_cases (p := s ⊆ (span K ↑(s' ∪ t) : Submodule K V))
        (fun this =>
          let ⟨u, hust, hsu, Eq⟩ := ih _ hs' hst this
          have hb₁u : b₁ ∉ u := fun h => (hust h).elim hb₁s hb₁t
          ⟨insert b₁ u, by simp [insert_subset_insert hust], Subset.trans hsu (by simp), by
            simp [Eq, hb₁t, hb₁s', hb₁u]⟩)
        fun this =>
        let ⟨b₂, hb₂s, hb₂t⟩ := not_subset.mp this
        have hb₂t' : b₂ ∉ s' ∪ t := fun h => hb₂t <| subset_span h
        have : s ⊆ (span K ↑(insert b₂ s' ∪ t) : Submodule K V) := fun b₃ hb₃ => by
          have : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t) : Set V) := by
            simp only [insert_eq, union_subset_union, Subset.refl,
              subset_union_right, Finset.union_insert, Finset.coe_insert]
          have hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t) : Set V)) :=
            span_mono this (hss' hb₃)
          have : s ⊆ (span K (insert b₁ ↑(s' ∪ t)) : Submodule K V) := by
            simpa [insert_eq, -singleton_union, -union_singleton] using hss'
          have hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t)) :=
            mem_span_insert_exchange (this hb₂s) hb₂t
          rw [span_insert_eq_span hb₁] at hb₃; simpa using hb₃
        let ⟨u, hust, hsu, eq⟩ := ih _ (by simp [insert_subset_iff, hb₂s, hs']) hst this
        ⟨u, Subset.trans hust <| union_subset_union (Subset.refl _) (by simp [subset_insert]), hsu,
          by simp [eq, hb₂t', hb₁t, hb₁s']⟩
  have eq : ((t.filter fun x => x ∈ s) ∪ t.filter fun x => x ∉ s) = t := by
    ext1 x
    by_cases x ∈ s <;> simp [*]
  apply
    Exists.elim
      (this (t.filter fun x => x ∉ s) (t.filter fun x => x ∈ s) (by simp [Set.subset_def])
        (by simp +contextual [Set.ext_iff]) (by rwa [eq]))
  intro u h
  exact
    ⟨u, Subset.trans h.1 (by simp +contextual [subset_def, or_imp]),
      h.2.1, by simp only [h.2.2, eq]⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
hB : B.Nonempty
hA1 : ∀ {a b : G}, a ∈ A → b ∈ A → a = b
hB1 : ∀ {a b : G}, a ∈ B → b ∈ B → a = b
a : G
ha : a ∈ A
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
obtain ⟨b, hb⟩ := hB

Goal state after:
G : Type u_1
inst✝ : Mul G
A B : Finset G
hA1 : ∀ {a b : G}, a ∈ A → b ∈ A → a = b
hB1 : ∀ {a b : G}, a ∈ B → b ∈ B → a = b
a : G
ha : a ∈ A
b : G
hb : b ∈ B
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
⊢ ⇑({i}ᶜ.orderEmbOfFin h) = ⇑(RelEmbedding.trans (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb)

Tactic:
rw [eq_comm]

Goal state after:
n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
⊢ ⇑(RelEmbedding.trans (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb) = ⇑({i}ᶜ.orderEmbOfFin h)
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case inr.intro.intro.left.refine_1
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #(A ×ˢ B)
hc' : #(image (⇑f) A ×ˢ image (⇑f) B) ≤ 1
p1 : H × H
h1 : p1 ∈ ↑(A ×ˢ B)
p2 : H × H
h2 : p2 ∈ ↑(A ×ˢ B)
hne : p1 ≠ p2
left✝¹ : p1.1 ∈ A
right✝¹ : p1.2 ∈ B
left✝ : p2.1 ∈ A
right✝ : p2.2 ∈ B
⊢ p1.1 ∈ A

Tactic:
assumption

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

Goal state before:
pp: case inr.intro.intro.left.refine_2
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #(A ×ˢ B)
hc' : #(image (⇑f) A ×ˢ image (⇑f) B) ≤ 1
p1 : H × H
h1 : p1 ∈ ↑(A ×ˢ B)
p2 : H × H
h2 : p2 ∈ ↑(A ×ˢ B)
hne : p1 ≠ p2
left✝¹ : p1.1 ∈ A
right✝¹ : p1.2 ∈ B
left✝ : p2.1 ∈ A
right✝ : p2.2 ∈ B
⊢ p1.2 ∈ B

Tactic:
assumption

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

Goal state before:
pp: case inr.intro.intro.right.refine_1
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #(A ×ˢ B)
hc' : #(image (⇑f) A ×ˢ image (⇑f) B) ≤ 1
p1 : H × H
h1 : p1 ∈ ↑(A ×ˢ B)
p2 : H × H
h2 : p2 ∈ ↑(A ×ˢ B)
hne : p1 ≠ p2
left✝¹ : p1.1 ∈ A
right✝¹ : p1.2 ∈ B
left✝ : p2.1 ∈ A
right✝ : p2.2 ∈ B
⊢ p2.1 ∈ A

Tactic:
assumption

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

Goal state before:
pp: case inr.intro.intro.right.refine_2
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #(A ×ˢ B)
hc' : #(image (⇑f) A ×ˢ image (⇑f) B) ≤ 1
p1 : H × H
h1 : p1 ∈ ↑(A ×ˢ B)
p2 : H × H
h2 : p2 ∈ ↑(A ×ˢ B)
hne : p1 ≠ p2
left✝¹ : p1.1 ∈ A
right✝¹ : p1.2 ∈ B
left✝ : p2.1 ∈ A
right✝ : p2.2 ∈ B
⊢ p2.2 ∈ B

Tactic:
assumption

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
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), TwoUniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := ⋯
A : Finset ((i : ι) → G i)
ihA :
  ∀ y ⊂ A,
    ∀ {B : Finset ((i : ι) → G i)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B : Finset ((i : ι) → G i)
⊢ ∀ (x : Finset ((i : ι) → G i)),
    (∀ y ⊂ x, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2) →
      1 < #A * #x → ∃ p1 ∈ A ×ˢ x, ∃ p2 ∈ A ×ˢ x, p1 ≠ p2 ∧ UniqueMul A x p1.1 p1.2 ∧ UniqueMul A x p2.1 p2.2

Tactic:
intro B ihB hc

Goal state after:
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), TwoUniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA :
  ∀ y ⊂ A,
    ∀ {B : Finset ((i : ι) → G i)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B✝ B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc : 1 < #A * #B
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h_exact : Function.Exact ⇑f ⇑g
h_surj : Surjective ⇑g
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R P
⊢ (map g ⊤).FG

Tactic:
rw [← LinearMap.range_eq_top] at h_surj
    rw [Submodule.map_top, h_surj]
    exact Module.Finite.fg_top

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred.WithBot

Goal state before:
pp: case bot
α : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : SuccAddOrder α
⊢ 1 ≤ ⊥ ↔ 0 < ⊥

Tactic:
simp [Order.one_le_iff_pos]

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred.WithBot

Goal state before:
pp: case coe
α : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : SuccAddOrder α
a✝ : α
⊢ 1 ≤ ↑a✝ ↔ 0 < ↑a✝

Tactic:
simp [Order.one_le_iff_pos]

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

Goal state before:
pp: R : Type u_8
N : Type u_10
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
Q : Submodule R N
⊢ Exact ⇑Q.subtype ⇑Q.mkQ

Tactic:
rw [exact_iff, Submodule.ker_mkQ, Submodule.range_subtype Q]

Goal state after: