mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case pos
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : Subtype p
h2 : f ↑i ≠ 0
⊢ (subtypeDomain p f) i = (mk (Finset.subtype p f.support) fun i ↦ f ↑↑i) i

Tactic:
simp at h2; simp [h2]

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

Goal state before:
pp: case neg
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : Subtype p
h2 : ¬f ↑i ≠ 0
⊢ (subtypeDomain p f) i = (mk (Finset.subtype p f.support) fun i ↦ f ↑↑i) i

Tactic:
simp at h2; simp [h2]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mp
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0
s : Finset ι
v : ι → N
hv : ∀ i ∈ s, v i ∈ p i
hv0 : ∑ i ∈ s, v i = 0
i : ι
⊢ i ∈ s → v i = 0

Tactic:
hi

Goal state after:
case mp
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0
s : Finset ι
v : ι → N
hv : ∀ i ∈ s, v i ∈ p i
hv0 : ∑ i ∈ s, v i = 0
i : ι
hi : i ∈ s
⊢ v i = 0
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval + l₂.eval = l.eval
⊢ l₁.eval + r₂ • x = r₂ • x + l₁.eval

Tactic:
rw [add_comm]

Goal state after:
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval + l₂.eval = l.eval
⊢ a₂.1 • a₂.2 + l₂.eval = l₂.eval + a₂.1 • a₂.2

Tactic:
rw [add_comm]

Goal state after:
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
⊢ l₁.eval + -(r₂ • x) = -(r₂ • x) + l₁.eval

Tactic:
rw [add_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: R : Type u_3
N : Type u_6
inst✝⁴ : Ring R
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
a : Π₀ (i : ι), ↥(p i) := (mapRange.linearMap fun i ↦ LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) l.toDFinsupp
ha : a = 0
i : ι
this : l i • v i = ↑(a i)
⊢ (fun x ↦ x • v i) (l i) = (fun x ↦ x • v i) (0 i)

Tactic:
simp only [coe_zero, Pi.zero_apply, ZeroMemClass.coe_zero, smul_eq_zero, ha] at this

Goal state after:
R : Type u_3
N : Type u_6
inst✝⁴ : Ring R
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
a : Π₀ (i : ι), ↥(p i) := (mapRange.linearMap fun i ↦ LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) l.toDFinsupp
ha : a = 0
i : ι
this : l i = 0 ∨ v i = 0
⊢ (fun x ↦ x • v i) (l i) = (fun x ↦ x • v i) (0 i)
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
c : S
⊢ LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]

Tactic:
by
  rcases subsingleton_or_nontrivial S with hS | hS; · simp [hS.elim c 0]
  nontriviality R
  simpa using pair_add_smul_add_smul_iff (x := x) (y := y) 1 0 c 1

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : AddCommMonoid α
f : κ → α
s : Finset κ
i : ι
⊢ ∑ g ∈ piFinset fun x ↦ s, f (g i) = #s ^ (card ι - 1) • ∑ b ∈ s, f b

Tactic:
classical
  rw [Finset.sum_comp]
  simp only [eval_image_piFinset_const, card_filter_piFinset_const s, ite_smul, zero_smul, smul_sum,
    Finset.sum_ite_mem, inter_self]

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)
⊢ Disjoint (span R (f i)) (⨆ i ∈ s, span R (f i))

Tactic:
exact hd i s s.finite_toSet his

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

Goal state before:
pp: case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
hImaximal : ∀ (t : Set ι), I ⊆ t → LinearIndepOn R v t → I = t
i : ι
⊢ i ∉ I → ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' I)

Tactic:
hi

Goal state after:
case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
hImaximal : ∀ (t : Set ι), I ⊆ t → LinearIndepOn R v t → I = t
i : ι
hi : i ∉ I
⊢ ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' I)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : f i • v i = -∑ x ∈ f.support.erase i, f x • v x
f_ne : f ≠ 0
hfi : f i ≠ 0
hfi' : i ∈ f.support
c : ι
hc : c ∈ f.support.erase i
⊢ c ∈ I

Tactic:
exact (memJ.mp (supp_f (Finset.erase_subset _ _ hc))).resolve_left (Finset.ne_of_mem_erase hc)

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

Goal state before:
pp: K : Type u_6
M : Type u_7
L : Type u_8
inst✝⁵ : CommSemiring K
inst✝⁴ : Semiring M
inst✝³ : Algebra K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ LinearIndependent L AlgHom.toLinearMap

Tactic:
by
  apply LinearIndependent.of_comp (LinearMap.ltoFun K M L L)
  exact (linearIndependent_monoidHom M L).comp
    (RingHom.toMonoidHom ∘ AlgHom.toRingHom)
    (fun _ _ e ↦ AlgHom.ext (DFunLike.congr_fun e :))

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝ : Semiring R
s : Set M
⊢ supported R R s = Submodule.span R ((fun m ↦ single m 1) '' s)

Tactic:
simp [supported_eq_map, Finsupp.supported_eq_span_single R s, Submodule.map_span,
    ← Set.image_comp]

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✝⁵ : CommSemiring S
inst✝⁴ : Monoid M
V : Type u_7
inst✝³ : AddCommMonoid V
inst✝² : Module S V
inst✝¹ : Module S[M] V
inst✝ : IsScalarTower S S[M] V
W : Submodule S V
h : ∀ (g : M), ∀ v ∈ W, (of S M) g • v ∈ W
f : S[M]
v : V
hv : v ∈ ↑W
⊢ f • v ∈ ↑W

Tactic:
← f.sum_coeff_single,

Goal state after:
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✝⁵ : CommSemiring S
inst✝⁴ : Monoid M
V : Type u_7
inst✝³ : AddCommMonoid V
inst✝² : Module S V
inst✝¹ : Module S[M] V
inst✝ : IsScalarTower S S[M] V
W : Submodule S V
h : ∀ (g : M), ∀ v ∈ W, (of S M) g • v ∈ W
f : S[M]
v : V
hv : v ∈ ↑W
⊢ f.coeff.sum single • v ∈ ↑W
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case refine_2
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
c : Set (Set ι)
hc : c ⊆ {b | b ⊆ t ∧ LinearIndepOn K v b}
cc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ LinearIndepOn K v (⋃₀ c)

Tactic:
exact linearIndepOn_sUnion_of_directed cc.directedOn fun x xc => (hc xc).2

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

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

Tactic:
exact image_image2_distrib_left h_distrib

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

Goal state before:
pp: R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x y : R[G]
g : G
⊢ (x * y).coeff g = x.coeff.sum fun h r ↦ r * y.coeff (h⁻¹ * g)

Tactic:
rw [coeff_mul]

Goal state after:
R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x y : R[G]
g : G
⊢ (x.coeff.sum fun m₁ r₁ ↦ y.coeff.sum fun m₂ r₂ ↦ if m₁ * m₂ = g then r₁ * r₂ else 0) =
    x.coeff.sum fun h r ↦ r * y.coeff (h⁻¹ * g)
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : ∀ ⦃a b c d : G⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
h : UniqueMul (image (⇑f) A) (image (⇑f) B) (f a0) (f b0)
a b : G
ha : a ∈ A
hb : b ∈ B
ab : a * b = a0 * b0
⊢ f a * f b = f a0 * f b0

Tactic:
simp_rw [← map_mul, ab]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ ↑(image f univ) = ↑s

Tactic:
coe_inj

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ image f univ = s
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
i j : Fin #s
⊢ (s.orderEmbOfFin ⋯) i = (s.orderEmbOfFin ⋯) j ↔ ↑i = ↑j

Tactic:
exact (s.orderEmbOfFin rfl).eq_iff_eq.trans Fin.ext_iff

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

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ {b} * {a} = {1}

Tactic:
← ha,

Goal state after:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
u : (Finset α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ {b} * ↑u = {1}
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
ht : 1 ∈ t
⊢ s ⊆ s * t⁻¹

Tactic:
exact subset_mul_left _ <| by simpa

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
L : Sublattice α
⊢ ↑L = ↑⊤ ↔ L = ⊤

Tactic:
coe_inj

Goal state after:
α : Type u_2
inst✝ : Lattice α
L : Sublattice α
⊢ L = ⊤ ↔ L = ⊤
Module: Mathlib.Order.Sublattice

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
L : Sublattice α
⊢ ↑L = ↑⊥ ↔ L = ⊥

Tactic:
coe_inj

Goal state after:
α : Type u_2
inst✝ : Lattice α
L : Sublattice α
⊢ L = ⊥ ↔ L = ⊥
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_2
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : UniqueProds G
inst✝ : UniqueProds H
⊢ UniqueProds (I G H false)

Tactic:
exact of_injective_mulHom (downMulHom G) down_injective ‹_›

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case fst
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
φ : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)
x : ↥p
⊢ ((fun φ ↦ (φ.domRestrict p, φ.domRestrict q)) ((ofIsComplProd h).toFun φ)).1 x = φ.1 x

Tactic:
exact ofIsCompl_apply_left h x

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' s = (Function.graph f).core s

Tactic:
simp [Set.preimage, SetRel.core]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case inr.inl
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ ((Fin.append p.toFun q.toFun ∘ Fin.cast ⋯)
        (Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length)).castSucc,
      (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯)
        (Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length)).succ) ∈
    r

Tactic:
convert! connect

Goal state after:
case e'_3
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯)
      (Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length)).castSucc =
    p.last

case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) (Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length)).succ =
    q.head
Module: Mathlib.Algebra.Group.UniqueProds.Basic

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

Tactic:
exact of_injective_mulHom (downMulHom G) down_injective ‹_›

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := ⋯
y : α := ⋯
hm : ↑i + 1 = ↑m
⊢ ↑m = ↑i.succ

Tactic:
exact hm.symm

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case h
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
i : ℕ
⊢ ∀ (h₁ : i < p.eraseLast.toList.length) (h₂ : i < p.toList.dropLast.length),
    p.eraseLast.toList[i] = p.toList.dropLast[i]

Tactic:
hi

Goal state after:
case h
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
i : ℕ
hi : i < p.eraseLast.toList.length
⊢ ∀ (h₂ : i < p.toList.dropLast.length), p.eraseLast.toList[i] = p.toList.dropLast[i]
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ height a + n = ⨆ p, ⨆ (_ : RelSeries.last p = a), ↑p.length + n

Tactic:
by
  have hne : Nonempty { p : LTSeries α // p.last = a } := ⟨RelSeries.singleton _ a, rfl⟩
  rw [height_eq_iSup_last_eq, iSup_subtype', iSup_subtype', ENat.iSup_add]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ ¬r.InfiniteDimensional ↔ r.FiniteDimensional

Tactic:
← not_finiteDimensional_iff,

Goal state after:
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ ¬¬r.FiniteDimensional ↔ r.FiniteDimensional
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ (RelSeries.eraseLast p).last < RelSeries.last p

Tactic:
exact p.eraseLast_last_rel_last (by lia)

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
⊢ 1 < height x ↔ ∃ y, ∃ z < y, y < x

Tactic:
← ENat.add_one_le_iff ENat.one_ne_top,

Goal state after:
α : Type u_1
inst✝ : Preorder α
x : α
⊢ 1 + 1 ≤ height x ↔ ∃ y, ∃ z < y, y < x
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
R'' : Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring R''
M : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R'' M
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : SMulCommClass R R'' M
x : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
⊢ 0 • 0 = 0

Tactic:
TensorProduct.smul_zero

Goal state after:
R : Type u_1
R'' : Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring R''
M : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R'' M
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : SMulCommClass R R'' M
x : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
R' : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : Monoid R'
M : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : DistribMulAction R' M
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : SMulCommClass R R' M
x : M ⊗[R] N
this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
⊢ 1 • 0 = 0

Tactic:
TensorProduct.smul_zero

Goal state after:
R : Type u_1
R' : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : Monoid R'
M : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : DistribMulAction R' M
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : SMulCommClass R R' M
x : M ⊗[R] N
this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁶ : CommSemiring R
inst✝³⁵ : CommSemiring R₂
inst✝³⁴ : CommSemiring R₃
inst✝³³ : Monoid R'
inst✝³² : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³¹ : AddCommMonoid M
inst✝³⁰ : AddCommMonoid N
inst✝²⁹ : AddCommMonoid P
inst✝²⁸ : AddCommMonoid Q
inst✝²⁷ : AddCommMonoid S
inst✝²⁶ : AddCommMonoid P'
inst✝²⁵ : AddCommMonoid Q'
inst✝²⁴ : AddCommMonoid M₂
inst✝²³ : AddCommMonoid N₂
inst✝²² : AddCommMonoid P₂
inst✝²¹ : AddCommMonoid Q₂
inst✝²⁰ : AddCommMonoid M₃
inst✝¹⁹ : AddCommMonoid N₃
inst✝¹⁸ : AddCommMonoid P₃
inst✝¹⁷ : AddCommMonoid Q₃
inst✝¹⁶ : DistribMulAction R' M
inst✝¹⁵ : Module R'' M
inst✝¹⁴ : Module R M
inst✝¹³ : Module R N
inst✝¹² : Module R S
inst✝¹¹ : Module R P'
inst✝¹⁰ : Module R Q'
inst✝⁹ : Module R₂ M₂
inst✝⁸ : Module R₂ N₂
inst✝⁷ : Module R₂ P₂
inst✝⁶ : Module R₂ Q₂
inst✝⁵ : Module R₃ M₃
inst✝⁴ : Module R₃ N₃
inst✝³ : Module R₃ P₃
inst✝² : Module R₃ Q₃
inst✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
r s : R'
x : M ⊗[R] N
⊢ (r * s) • 0 = r • s • 0

Tactic:
TensorProduct.smul_zero

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝⁴⁰ : CommSemiring R
inst✝³⁹ : CommSemiring R₂
inst✝³⁸ : CommSemiring R₃
inst✝³⁷ : Monoid R'
inst✝³⁶ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³⁵ : AddCommMonoid M
inst✝³⁴ : AddCommMonoid N
inst✝³³ : AddCommMonoid P
inst✝³² : AddCommMonoid Q
inst✝³¹ : AddCommMonoid S
inst✝³⁰ : AddCommMonoid P'
inst✝²⁹ : AddCommMonoid Q'
inst✝²⁸ : AddCommMonoid M₂
inst✝²⁷ : AddCommMonoid N₂
inst✝²⁶ : AddCommMonoid P₂
inst✝²⁵ : AddCommMonoid Q₂
inst✝²⁴ : AddCommMonoid M₃
inst✝²³ : AddCommMonoid N₃
inst✝²² : AddCommMonoid P₃
inst✝²¹ : AddCommMonoid Q₃
inst✝²⁰ : DistribMulAction R' M
inst✝¹⁹ : Module R'' M
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module R N
inst✝¹⁶ : Module R S
inst✝¹⁵ : Module R P'
inst✝¹⁴ : Module R Q'
inst✝¹³ : Module R₂ M₂
inst✝¹² : Module R₂ N₂
inst✝¹¹ : Module R₂ P₂
inst✝¹⁰ : Module R₂ Q₂
inst✝⁹ : Module R₃ M₃
inst✝⁸ : Module R₃ N₃
inst✝⁷ : Module R₃ P₃
inst✝⁶ : Module R₃ Q₃
inst✝⁵ : SMulCommClass R R' M
inst✝⁴ : SMulCommClass R R'' M
R'₂ : Type u_22
inst✝³ : Monoid R'₂
inst✝² : DistribMulAction R'₂ M
inst✝¹ : SMulCommClass R R'₂ M
inst✝ : SMulCommClass R' R'₂ M
r' : R'
r'₂ : R'₂
x : M ⊗[R] N
⊢ r' • r'₂ • 0 = r'₂ • r' • 0

Tactic:
TensorProduct.smul_zero

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
⊢ IsUnit ((Algebra.lmul R A) x) ↔ IsUnit x

Tactic:
rw [Module.End.isUnit_iff, Iff.comm]

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
⊢ IsUnit x ↔ Function.Bijective ⇑((Algebra.lmul R A) x)
Module: Mathlib.Order.KrullDimension

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

Tactic:
induction n using Nat.strong_induction_on generalizing x with

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

Goal state before:
pp: case le.refine_1
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
r : R
hr : r ∈ c.support
⊢ ↑((DistribSMul.toLinearMap R (↥N) r) (c r)) ∈ sInf {p | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p}

Tactic:
Submodule.mem_sInf

Goal state after:
case le.refine_1
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
r : R
hr : r ∈ c.support
⊢ ∀ p ∈ {p | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p}, ↑((DistribSMul.toLinearMap R (↥N) r) (c r)) ∈ p
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: case insert.mp
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
a : α
⊢ (∃ x ∈ f i, ∃ y, (∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = y) ∧ x * y = a) →
    ∃ g, ∃ (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a

pp: case insert.mpr
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
a : α
⊢ (∃ g, ∃ (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a) →
    ∃ x ∈ f i, ∃ y, (∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = y) ∧ x * y = a

Tactic:
· rintro ⟨x, y, hx, ⟨g, hg, rfl⟩, rfl⟩
      refine ⟨Function.update g i x, ?_, ?_⟩
      · intro j hj
        obtain rfl | hj := Finset.mem_insert.mp hj
        · rwa [Function.update_self]
        · rw [update_of_ne (ne_of_mem_of_not_mem hj hi)]
          exact hg hj
      · rw [Finset.prod_update_of_notMem hi, Function.update_self]

Goal state after:
case insert.mpr
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
a : α
⊢ (∃ g, ∃ (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a) →
    ∃ x ∈ f i, ∃ y, (∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = y) ∧ x * y = a