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

Goal state before:
pp: case h.cons.inl
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
i : ι
s : Multiset ι
ih : ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0), p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })
H3 :
  single i ({ toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } i) +
      erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } =
    { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }
h : f i = 0
⊢ p (single i (f i) + erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })

Tactic:
h,

Goal state after:
case h.cons.inl
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
i : ι
s : Multiset ι
ih : ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0), p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })
H3 :
  single i ({ toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } i) +
      erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } =
    { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }
h : f i = 0
⊢ p (single i 0 + erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
⊢ Function.Surjective (mapRange f hf) ↔ ∀ (i : ι), Function.Surjective (f i)

Tactic:
refine ⟨fun h i u ↦ ?_, fun h x ↦ ?_⟩

Goal state after:
case refine_1
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : Function.Surjective (mapRange f hf)
i : ι
u : β₂ i
⊢ ∃ a, f i a = u

case refine_2
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : ∀ (i : ι), Function.Surjective (f i)
x : Π₀ (i : ι), β₂ i
⊢ ∃ a, mapRange f hf a = x
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case refine_2.mk
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
this : ∀ (i : ι), ∃ u, f i u = x i ∧ (x i = 0 → u = 0)
⊢ ∃ a, mapRange f hf a = { toFun := x, support' := Quot.mk ⇑trueSetoid ⟨s, hs⟩ }

Tactic:
choose y hy using this

Goal state after:
case refine_2.mk
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
y : (i : ι) → β₁ i
hy : ∀ (i : ι), f i (y i) = x i ∧ (x i = 0 → y i = 0)
⊢ ∃ a, mapRange f hf a = { toFun := x, support' := Quot.mk ⇑trueSetoid ⟨s, hs⟩ }
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝²¹ : CommSemiring R
inst✝²⁰ : CommSemiring S
inst✝¹⁹ : SMul S R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : Module R N
inst✝¹⁴ : AddCommMonoid P
inst✝¹³ : Module R P
inst✝¹² : Module S M
inst✝¹¹ : Module S N
inst✝¹⁰ : Module S P
inst✝⁹ : IsScalarTower S R M
inst✝⁸ : IsScalarTower S R N
inst✝⁷ : IsScalarTower S R P
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module S M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module S N'
inst✝² : AddCommMonoid P'
inst✝¹ : Module S P'
inst✝ : SMulCommClass R S P
i : M' →ₗ[S] M
j : N' →ₗ[S] N
k : P' →ₗ[S] P
hk : Injective ⇑k
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ (m : M') (n : N'), (B (i m)) (j n) ∈ k.range
m : M'
n : N'
⊢ ((i.restrictScalarsRange₂ j k hk B hB) m) n = 0 ↔ (B (i m)) (j n) = 0

Tactic:
by
  rw [← hk.eq_iff, restrictScalarsRange₂_apply, map_zero]

Goal state after:
Module: Mathlib.Tactic.Module

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring S
inst✝² : Module S M
inst✝¹ : Ring R
inst✝ : Module R M
l : NF R M
l₀ : NF S M
hl : l.eval = l₀.eval
x : M
h : x = l₀.eval
⊢ -x = (-l).eval

Tactic:
h,

Goal state after:
S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring S
inst✝² : Module S M
inst✝¹ : Ring R
inst✝ : Module R M
l : NF R M
l₀ : NF S M
hl : l.eval = l₀.eval
x : M
h : x = l₀.eval
⊢ -l₀.eval = (-l).eval
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : 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
⊢ ?m.126

Tactic:
refine mt hImaximal ?_

Goal state after:
ι : 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
⊢ ¬I = J
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case pos
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
h : LinearIndepOn K f s
has : a ∈ s
⊢ f a ∈ span K (f '' s) ↔ LinearIndepOn K f (insert a s) → a ∈ s

Tactic:
exact iff_of_true (subset_span <| mem_image_of_mem f has) fun _ ↦ has

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ #(image₂ f s t) = #s * #t ↔ InjOn (fun x ↦ f x.1 x.2) (↑s ×ˢ ↑t)

Tactic:
rw [← card_product, ← coe_product]

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ #(image₂ f s t) = #(s ×ˢ t) ↔ InjOn (fun x ↦ f x.1 x.2) ↑(s ×ˢ t)
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
he : Injective ⇑f
⊢ Injective (map f)

Tactic:
have : map (M := M) f = coeffEquiv.symm ∘ Finsupp.mapRange f (map_zero f) ∘ coeffEquiv := by
    ext; simp [ofCoeff_mapRange]
  simpa [this] using mapRange_injective _ (map_zero f) he

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : ↑u ⊆ s ×ˢ t
⊢ ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ image (fun x ↦ f x.1 x.2) u ⊆ image₂ f s' t'

Tactic:
use u.image Prod.fst, u.image Prod.snd
  simp only [coe_image, Set.image_subset_iff, image₂_image_left, image₂_image_right,
    image_subset_iff]
  exact ⟨fun _ h ↦ (hu h).1, fun _ h ↦ (hu h).2, fun x hx ↦ mem_image₂_of_mem hx hx⟩

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

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝² : Semiring R
inst✝¹ : Monoid M
inst✝ : Monoid N
m : M
n : N
r : R
⊢ commRingEquiv (single m (single n r)) = single n (single m r)

Tactic:
by simp [commRingEquiv]

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

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
⊢ UniqueMul (map { toFun := op, inj' := ⋯ } (map { toFun := op, inj' := ⋯ } A))
    (map { toFun := op, inj' := ⋯ } (map { toFun := op, inj' := ⋯ } B)) (op (op a0)) (op (op b0))

Tactic:
simp_rw [map_map]

Goal state after:
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
⊢ UniqueMul (map ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) A)
    (map ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) B) (op (op a0)) (op (op b0))
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
a : α
n : ℕ
ha : a ∈ s
⊢ a ^ n ∈ s ^ n

Tactic:
by
  simpa using pow_subset_pow_left (singleton_subset_iff.2 ha)

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

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

Tactic:
h,

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R[X]
⊢ a.toFinsupp = 0 ↔ a = 0

Tactic:
by
  rw [← toFinsupp_zero, toFinsupp_inj]

Goal state after:
Module: Mathlib.Order.Sublattice

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

Tactic:
← coe_top,

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_bot,

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

Goal state before:
pp: κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
s : Set κ
L : (i : κ) → Sublattice (π i)
M : Sublattice ((i : κ) → π i)
⊢ M ≤ pi s L ↔ ∀ i ∈ s, M ≤ comap (Pi.evalLatticeHom i) (L i)

Tactic:
simp [SetLike.le_def]

Goal state after:
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
s : Set κ
L : (i : κ) → Sublattice (π i)
M : Sublattice ((i : κ) → π i)
⊢ (∀ ⦃x : (i : κ) → π i⦄, x ∈ M → ∀ i ∈ s, x i ∈ L i) ↔ ∀ i ∈ s, ∀ ⦃x : (i : κ) → π i⦄, x ∈ M → x i ∈ L i
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ (monomial n) r * X = (monomial (n + 1)) r

Tactic:
monomial_mul_X

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ (monomial (n + 1)) r = (monomial (n + 1)) r
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
n : ℕ
⊢ a • X ^ n = (monomial n) a

Tactic:
by
  rw [X_pow_eq_monomial, smul_monomial, smul_eq_mul, mul_one]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ (X ^ 1).support = {1}

Tactic:
support_X_pow 1

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ {1} = {1}
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case left
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 : (y : P) → y ∈ t1 → M
hg1 : ∀ (y : P) (a : y ∈ t1), g y a ∈ s
hg2 : ∀ (y : P) (a : y ∈ t1), f (g y a) = y
y : P
H : y ∈ t1
⊢ (fun y ↦ if H : y ∈ t1 then g y H else 0) y ∈ s

Tactic:
simp only [dif_pos H]

Goal state after:
case left
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 : (y : P) → y ∈ t1 → M
hg1 : ∀ (y : P) (a : y ∈ t1), g y a ∈ s
hg2 : ∀ (y : P) (a : y ∈ t1), f (g y a) = y
y : P
H : y ∈ t1
⊢ g y H ∈ s
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case right
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 : (y : P) → y ∈ t1 → M
hg1 : ∀ (y : P) (a : y ∈ t1), g y a ∈ s
hg2 : ∀ (y : P) (a : y ∈ t1), f (g y a) = y
y : P
H : y ∈ t1
⊢ f ((fun y ↦ if H : y ∈ t1 then g y H else 0) y) = y

Tactic:
simp only [dif_pos H]

Goal state after:
case right
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 : (y : P) → y ∈ t1 → M
hg1 : ∀ (y : P) (a : y ∈ t1), g y a ∈ s
hg2 : ∀ (y : P) (a : y ∈ t1), f (g y a) = y
y : P
H : y ∈ t1
⊢ f (g y H) = y
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
q : Submodule R E
F : Type u_7
inst✝¹ : AddCommGroup F
inst✝ : Module R F
i : F →ₗ[R] E
hi : Function.Injective ⇑i
h : IsCompl i.range q
x : F
⊢ (linearProjOfIsCompl q i hi h) (i x) = x

Tactic:
obtain ⟨ix, rfl⟩ := (LinearEquiv.ofInjective i hi).symm.surjective x

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
q : Submodule R E
F : Type u_7
inst✝¹ : AddCommGroup F
inst✝ : Module R F
i : F →ₗ[R] E
hi : Function.Injective ⇑i
h : IsCompl i.range q
ix : ↥i.range
⊢ (linearProjOfIsCompl q i hi h) (i ((LinearEquiv.ofInjective i hi).symm ix)) = (LinearEquiv.ofInjective i hi).symm ix
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inl
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
hι : IsEmpty ι
⊢ a * ⨅ i, f i = ⨅ i, a * f i

pp: case inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
hι : Nonempty ι
⊢ a * ⨅ i, f i = ⨅ i, a * f i

Tactic:
· suffices a ≠ 0 by simpa [iInf_of_empty, ite_eq_right_iff, mul_top']
    aesop

Goal state after:
case inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
hι : Nonempty ι
⊢ a * ⨅ i, f i = ⨅ i, a * f i
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inr
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
i j k : ι
hk : f i + g j ≤ f k + g k
⊢ f i + g j ≤ ⨆ i, f i + g i

Tactic:
exact le_iSup_of_le k hk

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
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:
rw [← hf.range, range_zero]

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

Goal state before:
pp: case refine_1
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : TwoUniqueProds G
inst✝ : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
⊢ TwoUniqueProds (G × H)

Tactic:
refine of_injective_mulHom (Prod.upMulHom G H) (fun x y he ↦ Prod.ext ?_ ?_)
      (TwoUniqueProds.instForall <| I G H) <;> apply up_injective

Goal state after:
case refine_1.refine_1
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : TwoUniqueProds G
inst✝ : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
x y : G × H
he : (Prod.upMulHom G H) x = (Prod.upMulHom G H) y
⊢ { down := x.1 } = { down := y.1 }

case refine_1.refine_2
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : TwoUniqueProds G
inst✝ : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
x y : G × H
he : (Prod.upMulHom G H) x = (Prod.upMulHom G H) y
⊢ { down := x.2 } = { down := y.2 }
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case pos
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
h : i.succ = Fin.last p.length
⊢ q.toFun 0 = p.toFun i.succ

Tactic:
h,

Goal state after:
case pos
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
h : i.succ = Fin.last p.length
⊢ q.toFun 0 = p.toFun (Fin.last p.length)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case top
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
ha : ¬∃ x, ∀ y ∈ Set.range fun x ↦ (↑x).length, y ≤ x
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Tactic:
contrapose! ha

Goal state after:
case top
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
ha : ∀ (p : LTSeries α), RelSeries.last p = a → p.length ≠ n
⊢ ∃ x, ∀ y ∈ Set.range fun x ↦ (↑x).length, y ≤ x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
h : ↑n < height x
⊢ ∃ y < x, height y = ↑n

Tactic:
obtain ⟨m, hx : height x = m⟩ := Option.ne_none_iff_exists'.mp hfin.ne_top

Goal state after:
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
h : ↑n < height x
m : ℕ
hx : height x = ↑m
⊢ ∃ y < x, height y = ↑n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ krullDim α ≤ 1 ↔ ∀ (x : α), IsMin x ∨ IsMax x

Tactic:
isMax_iff_forall_not_lt,

Goal state after:
α : Type u_1
inst✝ : Preorder α
⊢ krullDim α ≤ 1 ↔ ∀ (x : α), IsMin x ∨ ∀ (b : α), ¬x < b
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ 0 < krullDim α ↔ ∃ x y, x < y

Tactic:
by
  contrapose!
  simp_rw [← isMax_iff_forall_not_lt, ← krullDim_nonpos_iff_forall_isMax]

Goal state after:
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
r s : R''
x✝ : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
x y : M ⊗[R] N
ihx : (r + s) • x = r • x + s • x
ihy : (r + s) • y = r • y + s • y
⊢ (r + s) • (x + y) = r • (x + y) + s • (x + y)

Tactic:
TensorProduct.smul_add

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
r s : R''
x✝ : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
x y : M ⊗[R] N
ihx : (r + s) • x = r • x + s • x
ihy : (r + s) • y = r • y + s • y
⊢ (r + s) • x + (r + s) • y = r • x + r • y + (s • x + s • y)
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
n : N
hn : IsAddUnit n
m : M
⊢ IsAddUnit (m ⊗ₜ[R] n)

Tactic:
isAddUnit_iff_exists_neg

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
n : N
hn : ∃ b, n + b = 0
m : M
⊢ ∃ b, m ⊗ₜ[R] n + b = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
m : M
hm : IsAddUnit m
n : N
⊢ IsAddUnit (m ⊗ₜ[R] n)

Tactic:
isAddUnit_iff_exists_neg

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
m : M
hm : ∃ b, m + b = 0
n : N
⊢ ∃ b, m ⊗ₜ[R] n + b = 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✝ x y : M ⊗[R] N
ihx : (r * s) • x = r • s • x
ihy : (r * s) • y = r • s • y
⊢ (r * s) • (x + y) = r • s • (x + y)

Tactic:
TensorProduct.smul_add

Goal state after:
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✝ x y : M ⊗[R] N
ihx : (r * s) • x = r • s • x
ihy : (r * s) • y = r • s • y
⊢ (r * s) • x + (r * s) • y = r • s • x + r • s • y
Module: Mathlib.Order.KrullDimension

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

Tactic:
refine height_le_iff.mpr fun p hp ↦ le_of_not_gt fun h_len ↦ ?_

Goal state after:
case coe.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
⊢ False