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

Goal state before:
pp: case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
x : ι
a✝ : x ∈ s
hx : (DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x = 0
⊢ ↑0 = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
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₁ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
⊢ f₁.compl₁₂ g g' = f₁.compl₁₂ g g'

Tactic:
rfl

Goal state after:
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝¹ : AddMonoid M
inst✝ : SMul R M
p : R × M
l : NF R M
⊢ (p ::ᵣ l).eval = p.1 • p.2 + l.eval

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : 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
i : ι
hv0 : -v i = ∑ x ∈ s.erase i, v x
hi : i ∈ s
⊢ ∀ i_1 ∈ s.erase i, i_1 ≠ i

Tactic:
grind

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : 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
i : ι
hv0 : -v i = ∑ x ∈ s.erase i, v x
hi : i ∈ s
⊢ ∀ i_1 ∈ s.erase i, v i_1 ∈ p i_1

Tactic:
grind

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : 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
i : ι
f : ι →₀ N
hf : ∀ (i_1 : ι), f i_1 ∈ ⨆ (_ : i_1 ≠ i), p i_1
hx : (f.sum fun _i xi ↦ xi) ∈ p i
hsup : (f.sum fun _i xi ↦ xi) ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
h : (f.sum fun _i xi ↦ xi) ≠ 0
⊢ ∃ i_1 ∈ insert i f.support, (fun j ↦ if j = i then -f.sum fun x x_1 ↦ x_1 else f j) i_1 ≠ 0

Tactic:
grind

Goal state after:
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝¹ : SMul R M
inst✝ : AddGroup M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : l₁.eval - (a₂ ::ᵣ l₂).eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval - (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval

Tactic:
simp only [eval_cons, ← h, sub_eq_add_neg, add_assoc]

Goal state after:
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ Function.Injective ⇑(quotientInfToSupQuotient p p')

Tactic:
rw [← ker_eq_bot, quotientInfToSupQuotient, ker_liftQ_eq_bot]

Goal state after:
case h'
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ (subToSupQuotient p p').ker ≤ comap p.subtype (p ⊓ p')
Module: Mathlib.Tactic.Module

Goal state before:
pp: case h
S : Type u_1
R : Type u_2
M : Type u_3
R₀ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₀
inst✝² : Module R₀ M
inst✝¹ : Semiring S
inst✝ : Module S M
l : NF R M
l₀ : NF R₀ M
s : S
r : R
x : M
hx : x = l₀.eval
hl : l.eval = l₀.eval
hs : r • x = s • x
⊢ l.eval = l.eval

Tactic:
rfl

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
this : ∀ (x y : M), LinearIndependent R ![x, x + y] → LinearIndependent R ![x, y]
h : LinearIndependent R ![x, y]
⊢ LinearIndependent R ![x, x + y]

Tactic:
by simpa using this (-x) (x + y) (by simpa)

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

Goal state before:
pp: A : Type u_1
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : Monoid M
f : A → M
map_zero_eq_one' : f 0 = 1
map_add_eq_mul' : ∀ (a b : A), f (a + b) = f a * f b
⊢ ⇑{ toFun := f, map_zero_eq_one' := map_zero_eq_one', map_add_eq_mul' := map_add_eq_mul' } = f

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
φ ψ : AddChar A M
⊢ toMonoidHomEquiv.toFun (φ * ψ) = toMonoidHomEquiv.toFun φ * toMonoidHomEquiv.toFun ψ

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
φ ψ : Additive (AddChar A M)
⊢ toAddMonoidHomEquiv.toFun (φ + ψ) = toAddMonoidHomEquiv.toFun φ + toAddMonoidHomEquiv.toFun ψ

Tactic:
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
x y : V
⊢ x ∈ span K (insert y s) → x ∉ span K s → y ∈ span K (insert x s)

Tactic:
simp only [mem_span_insert, forall_exists_index, and_imp]
  rintro a z hz rfl h
  refine ⟨a⁻¹, -a⁻¹ • z, smul_mem _ _ hz, ?_⟩
  have a0 : a ≠ 0 := by
    rintro rfl
    simp_all
  match_scalars <;> simp [a0]

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
x : V
n : ℕ
v : Fin n → V
⊢ LinearIndependent K ((Fin.cons x v ∘ ⇑(finSuccEquiv n).symm) ∘ some) ∧
      (Fin.cons x v ∘ ⇑(finSuccEquiv n).symm) none ∉ span K (range ((Fin.cons x v ∘ ⇑(finSuccEquiv n).symm) ∘ some)) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : AddZeroClass M
f : S →+* R
g : Multiplicative M →* R
c : S
φ : S[M]
⊢ (liftNC ↑f ⇑g) (c • φ) = f c * (liftNC ↑f ⇑g) φ

Tactic:
by
  suffices (liftNC (↑f) g).comp (smulAddHom S S[M] c) =
      (AddMonoidHom.mulLeft (f c)).comp (liftNC f g) from DFunLike.congr_fun this φ
  ext
  simp [mul_assoc]

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
f : Fin 2 → V
⊢ Fin.tail f default = f (Fin.succ 0)

Tactic:
rfl

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 β
p : γ → Prop
⊢ (∀ z ∈ image₂ f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y)

Tactic:
by
  simp_rw [← mem_coe, coe_image₂, forall_mem_image2]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
t : Finset β
a : α
hf : Injective (f a)
⊢ #(image₂ f {a} t) = #t

Tactic:
rw [image₂_singleton_left, card_image_of_injective _ hf]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ (s.sup' ⋯ fun i ↦ t.sup' ⋯ fun i' ↦ (g ∘ uncurry f) (i, i')) = s.sup' ⋯ fun x ↦ t.sup' ⋯ fun x_1 ↦ g (f x x_1)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ (t.sup' ⋯ fun i' ↦ s.sup' ⋯ fun i ↦ (g ∘ uncurry f) (i, i')) = t.sup' ⋯ fun y ↦ s.sup' ⋯ fun x ↦ g (f x y)

Tactic:
rfl

Goal state after:
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
A : Type u_8
inst✝ : SMulZeroClass A R
⊢ SMul.smul = NSMul.nsmul

Tactic:
rfl

Goal state after:
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
A : Type u_8
inst✝¹ : SMulZeroClass A R
inst✝ : Monoid A
a : Aˣ
x : R[M]
⊢ a • x = ↑a • x

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
⊢ (s.sup fun i ↦ t.sup fun i' ↦ (g ∘ uncurry f) (i, i')) = s.sup fun x ↦ t.sup fun x_1 ↦ g (f x x_1)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
⊢ (t.sup fun i' ↦ s.sup fun i ↦ (g ∘ uncurry f) (i, i')) = t.sup fun y ↦ s.sup fun x ↦ g (f x y)

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
⊢ x * y = x.coeff.sum fun m₁ r₁ ↦ y.coeff.sum fun m₂ r₂ ↦ single (m₁ * m₂) (r₁ * r₂)

Tactic:
rfl

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

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
x2 y2 : G
h : UniqueMul A B x2 y2
hx hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = x2 * y2
⊢ (x2, y2) = (x2, y2)

Tactic:
rfl

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Mul G
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
h : UniqueMul A B a0 b0
p1 p2 : G × G
x✝¹ : (p1.1 ∈ A ∧ p1.2 ∈ B) ∧ p1.1 * p1.2 = a0 * b0
x✝ : (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p2.1 * p2.2 = a0 * b0
ha1 : p1.1 ∈ A
hb1 : p1.2 ∈ B
he1 : p1.1 * p1.2 = a0 * b0
ha2 : p2.1 ∈ A
hb2 : p2.2 ∈ B
he2 : p2.1 * p2.2 = a0 * b0
h1 : p1.1 = a0 ∧ p1.2 = b0
h2 : p2.1 = a0 ∧ p2.2 = b0
⊢ p1 = p2

Tactic:
grind

Goal state after:
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
f : G ↪ H
mul : ∀ (x y : G), f (x * y) = f x * f y
⊢ UniqueMul (image (⇑f) A) (image (⇑f) B) (f a0) (f b0) ↔
    UniqueMul (image (⇑{ toFun := ⇑f, map_mul' := mul }) A) (image (⇑{ toFun := ⇑f, map_mul' := mul }) B)
      ({ toFun := ⇑f, map_mul' := mul } a0) ({ toFun := ⇑f, map_mul' := mul } b0)

Tactic:
rfl

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
x✝¹ x✝ : G
⊢ ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) (x✝¹ * x✝) =
    ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) x✝¹ *
      ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) x✝

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ 0 < (s.sort fun a b ↦ a ≤ b).length

Tactic:
rw [length_sort]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ 0 < #s
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
n : ℕ
a : α
s : Fin n → Finset α
⊢ (∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a) ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a

Tactic:
rfl

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

Goal state before:
pp: case false
G : Type u
H : Type v
inst✝¹ : Mul G
inst✝ : Mul H
x y : G × H
⊢ (Bool.rec { down := (x * y).1 } { down := (x * y).2 } false).down =
    (((fun t ↦ Bool.rec { down := x.1 } { down := x.2 } t) * fun t ↦ Bool.rec { down := y.1 } { down := y.2 } t)
        false).down

Tactic:
rfl

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

Goal state before:
pp: case true
G : Type u
H : Type v
inst✝¹ : Mul G
inst✝ : Mul H
x y : G × H
⊢ (Bool.rec { down := (x * y).1 } { down := (x * y).2 } true).down =
    (((fun t ↦ Bool.rec { down := x.1 } { down := x.2 } t) * fun t ↦ Bool.rec { down := y.1 } { down := y.2 } t)
        true).down

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
a : α
⊢ span R (single a '' s) = span R (⇑(lsingle a) '' s)

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
a b : R[ℕ]
⊢ { toFinsupp := a + -b } = { toFinsupp := a } - { toFinsupp := b }

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
a b : R[X]
⊢ (a - b).toFinsupp = a.toFinsupp + -b.toFinsupp

Tactic:
rfl

Goal state after:
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)
⊢ (∀ ⦃x : (i : κ) → π i⦄, x ∈ M → ∀ i ∈ s, x i ∈ L i) ↔ ∀ i ∈ s, ∀ ⦃x : (i : κ) → π i⦄, x ∈ M → x i ∈ L i

Tactic:
grind

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

Goal state before:
pp: case e'_3.pq
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
x✝¹ : ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i
s : Finset (Submodule R M)
hsS : ↑s ⊆ S
hs : m ∈ ⨆ i ∈ s, i
x✝ : Submodule R M
⊢ x✝ ∈ s ↔ x✝ ∈ S ∧ x✝ ∈ s

Tactic:
grind

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

Goal state before:
pp: case ofFinsupp
R : Type u
inst✝ : Semiring R
i : ℕ
toFinsupp✝ : R[ℕ]
⊢ { toFinsupp := toFinsupp✝ }.toFinsupp.coeff i = { toFinsupp := toFinsupp✝ }.coeff i

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : GeneralLinearGroup R M
⊢ (f * g).toLinearEquiv = f.toLinearEquiv * g.toLinearEquiv

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
⊢ f⁻¹.toLinearEquiv = f.toLinearEquiv⁻¹

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M ≃ₗ[R] M
⊢ ofLinearEquiv (f * g) = ofLinearEquiv f * ofLinearEquiv g

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M ≃ₗ[R] M
⊢ ofLinearEquiv f⁻¹ = (ofLinearEquiv f)⁻¹

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : GeneralLinearGroup R M
x✝ : M
⊢ (x * y).toLinearEquiv x✝ = (x.toLinearEquiv * y.toLinearEquiv) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
x✝ : M
⊢ ↑((generalLinearEquiv R M) f) x✝ = ↑f x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
h : Nontrivial R[ℕ]
x y : R[ℕ]
hxy : x ≠ y
⊢ { toFinsupp := x } ≠ { toFinsupp := y }

Tactic:
simp [hxy]

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

Goal state before:
pp: R : Type u_1
ι : Type u_3
inst✝ : Semiring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
huv : IsCompl (Set.range u) (Set.range v)
this : IsCompl (span R (Set.range (⇑Finsupp.basisSingleOne ∘ u))) (span R (Set.range (⇑Finsupp.basisSingleOne ∘ v)))
⊢ IsCompl (span R (Set.range fun x ↦ single (u x) 1)) (span R (Set.range fun x ↦ single (v x) 1))

Tactic:
Function.comp_def

Goal state after:
R : Type u_1
ι : Type u_3
inst✝ : Semiring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
huv : IsCompl (Set.range u) (Set.range v)
this :
  IsCompl (span R (Set.range fun x ↦ Finsupp.basisSingleOne (u x))) (span R (Set.range (⇑Finsupp.basisSingleOne ∘ v)))
⊢ IsCompl (span R (Set.range fun x ↦ single (u x) 1)) (span R (Set.range fun x ↦ single (v x) 1))
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Module S N
inst✝¹ : SMulCommClass R S N
inst✝ : Module.Finite R M
s : Finset M
span_s : Submodule.span R ↑s = ⊤
x : M →ₗ[R] ι →₀ N
x✝ : M
a✝ : ι
⊢ (((finsuppLinearMap S) (onFinset (s.sup fun m ↦ (x m).support) (fun x_1 ↦ lapply x_1 ∘ₗ x) ⋯)) x✝) a✝ = (x x✝) a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_1
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝² : DecidableEq R
this✝¹ : DecidableEq M
this✝ : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
this : Inhabited P
⊢ (lmapDomain R R g) l = (lmapDomain R R g) l

Tactic:
rfl

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

Goal state before:
pp: case refine_2.refine_2
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
hA : A.Nonempty
hB : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
hc :
  (1 < #(image (fun x ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
    1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
p1 p2 : G i × G i
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p2.1 p2.2
a1 : (i : ι) → G i
ha1 : a1 ∈ A ∧ a1 i = p1.1
b1 : (i : ι) → G i
hb1 : b1 ∈ B ∧ b1 i = p1.2
hu1 : UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) a1 b1
a2 : (i : ι) → G i
ha2 : a2 ∈ A ∧ a2 i = p2.1
b2 : (i : ι) → G i
hb2 : b2 ∈ B ∧ b2 i = p2.2
hu2 : UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) a2 b2
⊢ (a1, b1) ≠ (a2, b2)

Tactic:
grind

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

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
⊢ a * ⨅ i, f i = ⨅ i, a * f i

Tactic:
refine (le_iInf fun x ↦ by grw [iInf_le]).antisymm ?_

Goal state after:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
⊢ ⨅ i, a * f i ≤ a * ⨅ i, f i
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
a : ℕ∞
κ : Sort u_4
q₁ : ι → Sort u_5
q₂ : κ → Sort u_6
f : (i : ι) → q₁ i → ℕ∞
g : (k : κ) → q₂ k → ℕ∞
h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk
⊢ a ≤ (⨅ i, ⨅ qi, f i qi) + ⨅ k, ⨅ qk, g k qk

Tactic:
by
  simp_rw [iInf₂_add, add_iInf₂]
  exact le_iInf₂ fun i hi => le_iInf₂ (h i hi)

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : E →ₗ[R] E
hp : IsIdempotentElem p
hq : IsIdempotentElem q
x✝ : p.range = q.range ∧ p.ker = q.ker
hr : p.range = q.range
hk : p.ker = q.ker
x : E
⊢ p x = q x

Tactic:
obtain ⟨⟨v, hv⟩, ⟨w, hw⟩, rfl, _⟩ :=
    (ker p).existsUnique_add_of_isCompl hp.isCompl.symm x

Goal state after:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : E →ₗ[R] E
hp : IsIdempotentElem p
hq : IsIdempotentElem q
x✝ : p.range = q.range ∧ p.ker = q.ker
hr : p.range = q.range
hk : p.ker = q.ker
v : E
hv : v ∈ p.ker
w : E
hw : w ∈ p.range
right✝ : ∀ (r : ↥p.ker) (s : ↥p.range), ↑r + ↑s = ↑⟨v, hv⟩ + ↑⟨w, hw⟩ → r = ⟨v, hv⟩ ∧ s = ⟨w, hw⟩
⊢ p (↑⟨v, hv⟩ + ↑⟨w, hw⟩) = q (↑⟨v, hv⟩ + ↑⟨w, hw⟩)
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
e : { e // f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e }
⊢ snd R M P ∘ₗ inr R M P = LinearMap.id

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_4
α : Type u_1
r : SetRel α α
s : RelSeries r
inst✝ : r.IsIrrefl
h : s.length ≠ 0
rid : s.toFun 0 = s.toFun 1
⊢ ↑1 = ↑⟨0, ⋯⟩.succ

Tactic:
simpa [Nat.pos_iff_ne_zero]

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).image s

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_2
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : i < Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length)
⊢ (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.castSucc =
    Fin.append p.toFun q.toFun (Fin.castAdd (q.length + 1) ⟨↑i, hi⟩.castSucc)

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_2
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : i < Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length)
⊢ (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.succ =
    Fin.append p.toFun q.toFun (Fin.castAdd (q.length + 1) ⟨↑i, hi⟩.succ)

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_2
α : 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 =
    Fin.append p.toFun q.toFun (Fin.natAdd (p.length + 1) 0)

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩
⊢ ↑y = ↑i + 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.RelSeries

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

Tactic:
grind

Goal state after: