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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ preBeth c.ord = c

Tactic:
by
  apply (preBeth_strictMono.comp ord_strictMono).le_apply.antisymm'
  apply (isNormal_preBeth.le_iff_forall_le (isSuccLimit_ord hc.aleph0_lt.le)).2
  refine fun a ha ↦ le_of_lt ?_
  induction a using WellFoundedLT.induction with | ind a IH
  rw [preBeth]
  apply lift_iSup_lt_of_lt_cof_ord _ _
  · rwa [mk_Iio_ordinal, lift_lift, hc.isRegular.lift.cof_ord, lift_lt, ← lt_ord]
  · rintro ⟨b, hb⟩
    exact hc.isStrongPrelimit <| IH _ hb (hb.trans ha)

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
h : p i
⊢ filter p (single i x) = single i x

Tactic:
by rw [filter_single, if_pos h]

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

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
l✝ : List ι
i : ι
l : List ι
C : ((i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)) → Prop
f : ∀ (a : (i_1 : ι) → i_1 ∈ i :: l → α i_1), C fun x1 x2 ↦ ⟦a x1 x2⟧
q : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
⊢ C q

Tactic:
by
    rw [← List.Pi.cons_eta q]
    induction List.Pi.head q using Quotient.ind with | _ a
    refine @list_ind _ (fun q ↦ C (List.Pi.cons _ _ ⟦a⟧ q)) ?_ (List.Pi.tail q)
    intro as
    rw [List.Pi.cons_map a as (fun i ↦ Quotient.mk (S i))]
    exact f _

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

Goal state before:
pp: case inl.inl
ι : 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 : ι) (j : α i), δ i j
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
fs : (i : ↥(↑s).toFinset) → { s_1 // ∀ (i_1 : α ↑i), i_1 ∈ s_1 ∨ (f ↑i).toFun i_1 = 0 }
i : ι
a : α i
hi : i ∈ ↑s
ha : a ∈ ↑(fs ⟨i, ⋯⟩)
⊢ (⟨i, a⟩ ∈ (↑s).toFinset.attach.val.bind fun i ↦ Multiset.map (Sigma.mk ↑i) ↑(fs i)) ∨ (f ⟨i, a⟩.fst) ⟨i, a⟩.snd = 0

Tactic:
left; rw [Multiset.mem_bind]
              use ⟨i, Multiset.mem_toFinset.mpr hi⟩
              constructor
              case right => simp [ha]
              case left => apply Multiset.mem_attach

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

Goal state before:
pp: case fst
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst✝ : (i : Option ι) → Zero (α i)
x : α none × Π₀ (i : ι), α (some i)
⊢ ((extendWith x.1 x.2) none, comapDomain some ⋯ (extendWith x.1 x.2)).1 = x.1

pp: case snd
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst✝ : (i : Option ι) → Zero (α i)
x : α none × Π₀ (i : ι), α (some i)
i✝ : ι
⊢ ((extendWith x.1 x.2) none, comapDomain some ⋯ (extendWith x.1 x.2)).2 i✝ = x.2 i✝

Tactic:
· exact extendWith_none x.snd _

Goal state after:
case snd
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst✝ : (i : Option ι) → Zero (α i)
x : α none × Π₀ (i : ι), α (some i)
i✝ : ι
⊢ ((extendWith x.1 x.2) none, comapDomain some ⋯ (extendWith x.1 x.2)).2 i✝ = x.2 i✝
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case refine_2
ι : 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
⊢ x ∈ AddMonoidHom.mrange (mapRange.addMonoidHom f)

Tactic:
use DFinsupp.mk x.support (g ·)

Goal state after:
case h
ι : 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
⊢ (mapRange.addMonoidHom f) (mk x.support fun x_1 ↦ g ↑x_1) = x
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : Set η
t : η → Set ι
hs : DirectedOn (t ⁻¹'o fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v (t a)
⊢ LinearIndepOn R v (⋃ x, t ↑x)

Tactic:
exact linearIndepOn_iUnion_of_directed (directed_comp.2 <| hs.directed_val) (by simpa using h)

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
N : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : AddCommGroup N
p : ι → AddSubgroup N
h : Function.Injective ⇑(sumAddHom fun i ↦ (p i).subtype)
⊢ iSupIndep p

Tactic:
by
  rw [← iSupIndep_map_orderIso_iff (AddSubgroup.toIntSubmodule : AddSubgroup N ≃o _)]
  exact iSupIndep_of_dfinsupp_lsum_injective _ h

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • u • x + t • u • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ u • s • x + u • t • y = 0

Tactic:
← smul_add,

Goal state after:
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
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • u • x + t • u • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ u • (s • x + t • y) = 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
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ d • a • s + d • c • t = 0

Tactic:
← smul_add,

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

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

Tactic:
← smul_add,

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
ind : iSupIndep p
iSup_top : ⨆ i, p i = ⊤
⊢ ((lsum ℕ) fun i ↦ (p i).subtype).range = ⊤

Tactic:
← Submodule.iSup_eq_range_dfinsupp_lsum

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
ind : iSupIndep p
iSup_top : ⨆ i, p i = ⊤
⊢ iSup p = ⊤
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

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

Tactic:
← smul_add,

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

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

Tactic:
← smul_add,

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

Goal state before:
pp: X : Type u_1
k : ℕ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ (k • a).support = a.support

Tactic:
by
  apply support_zsmul k _ a
  exact mod_cast h

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

Goal state before:
pp: case h.insert
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
i : ι
s : Finset ι
his : i ∉ s
ih : LinearIndepOn R id (⋃ i ∈ s, f i)
⊢ LinearIndepOn R id (⋃ i_1 ∈ insert i s, f i_1)

Tactic:
| insert i s his ih =>

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)
x : M
hx : f x = 0
⊢ x ∈ span R (Set.range v)

Tactic:
rw [hv]

Goal state after:
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)
x : M
hx : f x = 0
⊢ x ∈ ⊤
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ : AddChar A M
a : A
⊢ ψ⁻¹ a = (ψ a)⁻¹

Tactic:
inv_apply,

Goal state after:
A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ : AddChar A M
a : A
⊢ ψ (-a) = (ψ a)⁻¹
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
x✝ : R
⊢ ψ⁻¹ x✝ = (ψ.mulShift (-1)) x✝

Tactic:
inv_apply,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
x✝ : R
⊢ ψ (-x✝) = (ψ.mulShift (-1)) x✝
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝ : Mul M
⊢ ∀ (a b c : R[M]), a * (b + c) = a * b + a * c

Tactic:
classical simp [mul_def, mul_add, sum_add, sum_add_index]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
j : Fin k
⊢ ({i}ᶜ.orderEmbOfFin h) j = i.succAbove (Fin.cast ⋯ j)

Tactic:
rw [orderEmbOfFin_compl_singleton]
  simp

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

Goal state before:
pp: case pos
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 D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
h12 : c1 ≠ 1 ∨ d2 ≠ 1
c3 d3 : G
hu : d1⁻¹ * (c3 * (d3 * c2⁻¹)) = d1⁻¹ * c1 * (d2 * c2⁻¹) → c3 = c1 ∧ d3 = d2
hc3 : c3 ∈ C
hd3 : d3 ∈ D
he : c3 * d3 = c1 * d2
⊢ c3 = c1 ∧ d3 = d2

Tactic:
← mul_assoc c3,

Goal state after:
case pos
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 D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
h12 : c1 ≠ 1 ∨ d2 ≠ 1
c3 d3 : G
hu : d1⁻¹ * (c3 * d3 * c2⁻¹) = d1⁻¹ * c1 * (d2 * c2⁻¹) → c3 = c1 ∧ d3 = d2
hc3 : c3 ∈ C
hd3 : d3 ∈ D
he : c3 * d3 = c1 * d2
⊢ c3 = c1 ∧ d3 = d2
Module: Mathlib.RingTheory.Finiteness.Cardinality

Goal state before:
pp: M : Type u_3
inst✝ : AddCommGroup M
H : AddSubgroup M
⊢ H.FG ↔ ∃ n f, f.range = H

Tactic:
rw [← H.toIntSubmodule_toAddSubgroup, ← Submodule.fg_iff_addSubgroup_fg,
    Submodule.fg_iff_exists_fin_linearMap]

Goal state after:
M : Type u_3
inst✝ : AddCommGroup M
H : AddSubgroup M
⊢ (∃ n f, f.range = toIntSubmodule H) ↔ ∃ n f, f.range = (toIntSubmodule H).toAddSubgroup
Module: Mathlib.RingTheory.Finiteness.Cardinality

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite R
s : Set M
hs : s.Finite
⊢ (↑(span R s)).Finite

Tactic:
by
  lift s to Finset M using hs
  rw [Set.Finite, ← Module.finite_iff_finite (R := R)]
  dsimp
  infer_instance

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

Goal state before:
pp: case inr.hx
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 : β
⊢ Finsupp.basisSingleOne (v i) ∈ span R (Set.range fun x ↦ single (v x) 1)

Tactic:
exact Submodule.subset_span ⟨i, rfl⟩

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

Goal state before:
pp: case inr.intro.intro
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
⊢ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
constructor <;> refine UniqueMul.of_mulHom_image f hf
      ((UniqueMul.iff_card_le_one ?_ ?_).mpr <| (card_filter_le _ _).trans hc') <;>
    apply mem_image_of_mem <;> assumption

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: 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

Tactic:
rw [range_subtype, range_subtype]

Goal state after:
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 q
Module: Mathlib.LinearAlgebra.Projection

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

Tactic:
Submodule.add_mem_iff_right _ (Submodule.coe_mem _),

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

Goal state before:
pp: 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
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective ⇑f
⊢ (comap f g.ker).FG

Tactic:
apply fg_of_fg_map_of_fg_inf_ker f

Goal state after:
case hs1
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
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective ⇑f
⊢ (map f (comap f g.ker)).FG

case hs2
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
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective ⇑f
⊢ (comap f g.ker ⊓ f.ker).FG
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: σ : Type u_1
inst✝ : Finite σ
⊢ AddMonoid.FG (FreeAbelianGroup σ)

Tactic:
by
  rw [← AddGroup.fg_iff_addMonoid_fg, ← Module.Finite.iff_addGroup_fg]; infer_instance

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_1
f : ι → ℕ∞
n : ℕ
⊢ ⨅ i, f i = ↑n ↔ (∃ i, f i = ↑n) ∧ ∀ (i : ι), ↑n ≤ f i

Tactic:
by_cases! hι : IsEmpty ι

Goal state after:
case pos
ι : Sort u_1
f : ι → ℕ∞
n : ℕ
hι : IsEmpty ι
⊢ ⨅ i, f i = ↑n ↔ (∃ i, f i = ↑n) ∧ ∀ (i : ι), ↑n ≤ f i

case neg
ι : Sort u_1
f : ι → ℕ∞
n : ℕ
hι : Nonempty ι
⊢ ⨅ i, f i = ↑n ↔ (∃ i, f i = ↑n) ∧ ∀ (i : ι), ↑n ≤ f i
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_1
f : ι → ℕ∞
n : ℕ
⊢ ⨅ i, f i = ↑n ↔ (∃ i, f i = ↑n) ∧ ∀ (i : ι), ↑n ≤ f i

Tactic:
by_cases! hι : IsEmpty ι
  · simp [iInf_of_isEmpty]
  apply ciInf_eq_iff

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
x✝ : M
⊢ f x✝ = 0 x✝

Tactic:
simpa using hf.map_mem _

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ (p.append q connect).toList = p.toList ++ q.toList

Tactic:
apply List.ext_getElem
  · simp; grind
  · simp [List.getElem_append, Fin.append, Fin.addCases]

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalHom

Goal state before:
pp: R : Type u
S : Type u₁
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
φ : R →* S
A : Type v
B : Type w
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : DistribMulAction S B
f g : A →ₛₙₐ[φ] B
h : ↑f = ↑g
⊢ f = g

Tactic:
ext a
  exact DistribMulActionHom.congr_fun h a

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last = q.head
i : Fin (p.length + 1)
⊢ (p.smash q h).toFun (Fin.castLE ⋯ i) = p.toFun i

Tactic:
by
  refine i.lastCases ?_ fun _ ↦ by dsimp only [smash]; apply Fin.addCases_left
  change p.smash q h (Fin.natAdd p.length (0 : Fin (q.length + 1))) = _
  simpa only [smash, Fin.addCases_right] using! h.symm

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x = ↑n + 1 ↔ (∃ y < x, height y = ↑n) ∧ ∀ y < x, height y ≤ ↑n

Tactic:
trans n < height x ∧ height x ≤ n + 1

Goal state after:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x = ↑n + 1 ↔ ↑n < height x ∧ height x ≤ ↑n + 1

α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ ↑n < height x ∧ height x ≤ ↑n + 1 ↔ (∃ y < x, height y = ↑n) ∧ ∀ y < x, height y ≤ ↑n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
p' : LTSeries α :=
  { length := p.length - 1,
    toFun := fun x ↦
      match x with
      | ⟨i, hi⟩ => (p.toFun ⟨i + 1, ⋯⟩).unbot ⋯,
    step := ⋯ }
⊢ RelSeries.last p' = x

Tactic:
simp only [p', RelSeries.last, WithBot.unbot_eq_iff, ← hlast, Fin.last]

Goal state after:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
p' : LTSeries α :=
  { length := p.length - 1,
    toFun := fun x ↦
      match x with
      | ⟨i, hi⟩ => (p.toFun ⟨i + 1, ⋯⟩).unbot ⋯,
    step := ⋯ }
⊢ p.toFun ⟨p.length - 1 + 1, ⋯⟩ = p.toFun ⟨p.length, ⋯⟩
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
⊢ -0 + 0 = 0

Tactic:
rw [add_zero]; apply (Neg.aux R).map_zero

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
x : α
⊢ coheight x ≤ (↑m + 1) * coheight (f x) + ↑m

Tactic:
rw [Order.coheight, Order.coheight]
  apply height_le_of_krullDim_preimage_le (f := f.dual)
  exact fun x ↦ le_of_eq_of_le (krullDim_orderDual (α := f ⁻¹' {x})) (h x)

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

Goal state before:
pp: case cons
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f₁ f₂ : ι → Set α
h : ι
tl : List ι
ih : (∀ i ∈ tl, f₁ i ⊆ f₂ i) → (List.map f₁ tl).prod ⊆ (List.map f₂ tl).prod
hf : ∀ i ∈ h :: tl, f₁ i ⊆ f₂ i
⊢ f₁ h * (List.map f₁ tl).prod ⊆ f₂ h * (List.map f₂ tl).prod

Tactic:
exact mul_subset_mul (hf h List.mem_cons_self)
      (ih fun i hi ↦ hf i <| List.mem_cons_of_mem _ hi)

Goal state after:
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (z * x + y)

Tactic:
by
  rw [add_comm]
  exact h.add_mul_right_right z

Goal state after: