mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : Nontrivial R
h : a * d = b * c
hbd : b = 0 ∧ d = 0
hac : ¬(a = 0 ∧ c = 0)
⊢ c • 1 = 0 → -a • 1 ≠ 0

Tactic:
aesop

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

Goal state before:
pp: X : Type u_1
k : ℕ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ ↑k ≠ 0

Tactic:
exact mod_cast h

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : AddCommMonoid α
R : Type u_7
inst✝¹ : Semiring R
inst✝ : Module R α
f : ι → α
r : R
i₀ : ι
⊢ Pi.single i₀ r i₀ • f i₀ = r • f i₀

pp: case h₀
ι : Type u_1
α : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : AddCommMonoid α
R : Type u_7
inst✝¹ : Semiring R
inst✝ : Module R α
f : ι → α
r : R
i₀ : ι
⊢ ∀ b ∈ univ, b ≠ i₀ → Pi.single i₀ r b • f b = 0

pp: case h₁
ι : Type u_1
α : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : AddCommMonoid α
R : Type u_7
inst✝¹ : Semiring R
inst✝ : Module R α
f : ι → α
r : R
i₀ : ι
⊢ i₀ ∉ univ → Pi.single i₀ r i₀ • f i₀ = 0

Tactic:
Pi.single_eq_same

Goal state after:
ι : Type u_1
α : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : AddCommMonoid α
R : Type u_7
inst✝¹ : Semiring R
inst✝ : Module R α
f : ι → α
r : R
i₀ : ι
⊢ r • f i₀ = r • f i₀

case h₀
ι : Type u_1
α : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : AddCommMonoid α
R : Type u_7
inst✝¹ : Semiring R
inst✝ : Module R α
f : ι → α
r : R
i₀ : ι
⊢ ∀ b ∈ univ, b ≠ i₀ → Pi.single i₀ r b • f b = 0

case h₁
ι : Type u_1
α : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : AddCommMonoid α
R : Type u_7
inst✝¹ : Semiring R
inst✝ : Module R α
f : ι → α
r : R
i₀ : ι
⊢ i₀ ∉ univ → Pi.single i₀ r i₀ • f i₀ = 0
Module: Mathlib.Algebra.Module.BigOperators

Goal state before:
pp: case h₀
ι : Type u_1
α : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : AddCommMonoid α
R : Type u_7
inst✝¹ : Semiring R
inst✝ : Module R α
f : ι → α
r : R
i₀ : ι
⊢ ∀ b ∈ univ, b ≠ i₀ → Pi.single i₀ r b • f b = 0

Tactic:
aesop

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

Goal state before:
pp: case h₁
ι : Type u_1
α : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : AddCommMonoid α
R : Type u_7
inst✝¹ : Semiring R
inst✝ : Module R α
f : ι → α
r : R
i₀ : ι
⊢ i₀ ∉ univ → Pi.single i₀ r i₀ • f i₀ = 0

Tactic:
aesop

Goal state after:
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
⊢ ∃ s, LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' s)

Tactic:
rcases exists_maximal_linearIndepOn' R v with ⟨I, hIlinind, 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
hImaximal : ∀ (t : Set ι), I ⊆ t → LinearIndepOn R v t → I = t
⊢ ∃ s, LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' s)
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) ↔ LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
← linearIndependent_equiv (finSuccEquiv n).symm,

Goal state after:
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) ↔ LinearIndependent K v ∧ x ∉ span K (range v)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_6
K : Type u_7
M : Type u_8
inst✝⁷ : CommRing R
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R K
inst✝³ : Module K M
inst✝² : Module R M
inst✝¹ : IsScalarTower R K M
inst✝ : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : y ∈ span R (range v)
heq : (algebraMap R K) c • x + y = 0
hc : ¬c = 0
hc' : (algebraMap R K) c ≠ 0
⊢ -(((algebraMap R K) c)⁻¹ • y) ∈ span K (range v)

Tactic:
exact Submodule.neg_mem _ (Submodule.smul_mem _ _ (Submodule.span_subset_span R K _ hcy))

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

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

Tactic:
refine zorn_subset_nonempty { b | b ⊆ t ∧ LinearIndepOn K v b} ?_ _ ⟨hst, hs⟩

Goal state after:
ι : 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 ⊆ {b | b ⊆ t ∧ LinearIndepOn K v b},
    IsChain (fun x1 x2 ↦ x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ {b | b ⊆ t ∧ LinearIndepOn K v b}, ∀ s ∈ c, s ⊆ ub
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a ↦ f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a ↦ ⟨v ↑a, ⋯⟩
⊢ range (v ∘ Subtype.val) = t

Tactic:
aesop

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

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
N : Type u_7
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : Monoid M
inst✝ : Monoid N
f : R →+* S
g : M →* N
⊢ (mapRingHom N f).comp (mapDomainRingHom R g) = (mapDomainRingHom S g).comp (mapRingHom M f)

Tactic:
aesop

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 β
hf : ∀ b ∈ t, Injective fun a ↦ f a b
ht : ((fun b ↦ image (fun a ↦ f a b) s) '' ↑t).PairwiseDisjoint id
⊢ #s ∣ #(image₂ f s t)

Tactic:
by rw [← image₂_swap]; exact card_dvd_card_image₂_right hf ht

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

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

Tactic:
exact hfs x

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
a : α
n : ℤ
⊢ {a} ^ n = {a ^ n}

Tactic:
by cases n <;> simp

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

Goal state before:
pp: α : Type u_2
inst✝² : Mul α
inst✝¹ : IsLeftCancelMul α
inst✝ : DecidableEq α
s : Finset α
⊢ #s ≤ #(s * s)

Tactic:
cases s.eq_empty_or_nonempty

Goal state after:
case inl
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsLeftCancelMul α
inst✝ : DecidableEq α
s : Finset α
h✝ : s = ∅
⊢ #s ≤ #(s * s)

case inr
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsLeftCancelMul α
inst✝ : DecidableEq α
s : Finset α
h✝ : s.Nonempty
⊢ #s ≤ #(s * s)
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Mul α
inst✝¹ : IsRightCancelMul α
inst✝ : DecidableEq α
s : Finset α
⊢ #s ≤ #(s * s)

Tactic:
cases s.eq_empty_or_nonempty

Goal state after:
case inl
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsRightCancelMul α
inst✝ : DecidableEq α
s : Finset α
h✝ : s = ∅
⊢ #s ≤ #(s * s)

case inr
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsRightCancelMul α
inst✝ : DecidableEq α
s : Finset α
h✝ : s.Nonempty
⊢ #s ≤ #(s * s)
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s : Finset α
⊢ #s ≤ #(s / s)

Tactic:
cases s.eq_empty_or_nonempty

Goal state after:
case inl
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s : Finset α
h✝ : s = ∅
⊢ #s ≤ #(s / s)

case inr
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s : Finset α
h✝ : s.Nonempty
⊢ #s ≤ #(s / s)
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
σ : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
φ : M →ₗ[R] N
f : σ → R
⊢ map ((lsum R) fun x ↦ f x • φ) (span R {x | ∃ i x_1, single i x_1 = x}) = Set.range f • map φ ⊤

Tactic:
← span_univ,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
σ : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
φ : M →ₗ[R] N
f : σ → R
⊢ map ((lsum R) fun x ↦ f x • φ) (span R {x | ∃ i x_1, single i x_1 = x}) = Set.range f • map φ (span R univ)
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).support = p.support

Tactic:
by simp [support]

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 q

Tactic:
exact h.1

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

Goal state before:
pp: M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : MulExact ⇑f ⇑g
x₂ : M₂
x₁ : M₁
hy₁ : f' (τ₁ x₁) = τ₂ x₂
⊢ x₂ ∈ Set.range ⇑f

Tactic:
exact ⟨x₁, h₂.1 (by simpa only [comm₁₂] using hy₁)⟩

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

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

Tactic:
aesop

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

Goal state before:
pp: case mpr.mp
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : MulExact ⇑f' ⇑g'
x₂ : M₂
hx₂ : g x₂ = 1
x₁ : M₁
hy₁ : f' (τ₁ x₁) = τ₂ x₂
⊢ x₂ ∈ Set.range ⇑f

Tactic:
exact ⟨x₁, h₂.1 (by simpa only [comm₁₂] using hy₁)⟩

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

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

Tactic:
exact_iff,

Goal state after:
R : Type u_8
N : Type u_10
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
Q : Submodule R N
⊢ Q.mkQ.ker = Q.subtype.range
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
⊢ a + iInf f = ⨅ b, a + f b

Tactic:
by
  rw [add_comm, iInf_add]; simp [add_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
hf : IsProj m f
⊢ m = ⊤ ↔ f = id

Tactic:
by
  constructor <;> rintro rfl
  · ext
    simp [hf.map_id]
  · rw [← hf.range, range_id]

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ ∅.dom = ∅

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ ∅.cod = ∅

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty β
⊢ dom Set.univ = Set.univ

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty α
⊢ cod Set.univ = Set.univ

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
⊢ SetRel.id.inv = SetRel.id

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R : SetRel α β
S : SetRel β γ
t : SetRel γ δ
⊢ R ○ S ○ t = R ○ (S ○ t)

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R ○ SetRel.id = R

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ SetRel.id ○ R = R

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
S : SetRel β γ
⊢ (R ○ S).inv = S.inv ○ R.inv

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
⊢ R ○ ∅ = ∅

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
S : SetRel β γ
⊢ ∅ ○ S = ∅

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
⊢ R ○ Set.univ = {(a, _c) | a ∈ R.dom}

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
S : SetRel β γ
⊢ Set.univ ○ S = {(_b, c) | c ∈ S.cod}

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
R : SetRel α β
S : ι → SetRel β γ
⊢ R ○ ⋃ i, S i = ⋃ i, R ○ S i

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
R : ι → SetRel α β
S : SetRel β γ
⊢ (⋃ i, R i) ○ S = ⋃ i, R i ○ S

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
𝒮 : Set (SetRel β γ)
⊢ R ○ ⋃₀ 𝒮 = ⋃ S ∈ 𝒮, R ○ S

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ℛ : Set (SetRel α β)
S : SetRel β γ
⊢ ⋃₀ ℛ ○ S = ⋃ R ∈ ℛ, R ○ S

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t₁ t₂ : Set β
ht : (t₁ ∩ t₂).Nonempty
s : Set α
u : Set γ
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = s ×ˢ u

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R.image ∅ = ∅

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R.preimage ∅ = ∅

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R.image Set.univ = R.cod

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R.preimage Set.univ = R.dom

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
s₁ s₂ : Set α
⊢ R.image (s₁ ∪ s₂) = R.image s₁ ∪ R.image s₂

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
R : SetRel α β
s : ι → Set α
⊢ R.image (⋃ i, s i) = ⋃ i, R.image (s i)

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
S : Set (Set α)
⊢ R.image (⋃₀ S) = ⋃ s ∈ S, R.image s

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
t₁ t₂ : Set β
⊢ R.preimage (t₁ ∪ t₂) = R.preimage t₁ ∪ R.preimage t₂

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
R : SetRel α β
t : ι → Set β
⊢ R.preimage (⋃ i, t i) = ⋃ i, R.preimage (t i)

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
T : Set (Set β)
⊢ R.preimage (⋃₀ T) = ⋃ t ∈ T, R.preimage t

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
s : Set α
⊢ SetRel.id.image s = s

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
s : Set α
⊢ SetRel.id.preimage s = s

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
S : SetRel β γ
s : Set α
⊢ (R ○ S).image s = S.image (R.image s)

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
S : SetRel β γ
u : Set γ
⊢ (R ○ S).preimage u = R.preimage (S.preimage u)

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
⊢ ∅.image s = ∅

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
⊢ ∅.preimage t = ∅

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
hs : s.Nonempty
⊢ image Set.univ s = Set.univ

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
ht : t.Nonempty
⊢ preimage Set.univ t = Set.univ

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
s : Set α
h : R.dom ⊆ s
⊢ R.image s = R.cod

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
t : Set β
h : R.cod ⊆ t
⊢ R.preimage t = R.dom

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
s : Set α
⊢ R.image (s ∩ R.dom) = R.image s

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
t : Set β
⊢ R.preimage (t ∩ R.cod) = R.preimage t

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
s : Set α
⊢ R.image s = ⋃ x ∈ s, {y | (x, y) ∈ R}

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
t : Set β
⊢ R.preimage t = ⋃ y ∈ t, {x | (x, y) ∈ R}

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
t₁ t₂ : Set β
⊢ R.core (t₁ ∩ t₂) = R.core t₁ ∩ R.core t₂

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R.core Set.univ = Set.univ

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: β : Type u_2
t : Set β
⊢ SetRel.id.core t = t

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
S : SetRel β γ
u : Set γ
⊢ (R ○ S).core u = R.core (S.core u)

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
f : E →ₗ[R] E
hf : IsIdempotentElem f
T : (E →ₗ[R] E)ˣ
⊢ Commute f ↑((GeneralLinearGroup.generalLinearEquiv R E) T) ↔
    (f.range ∈ Module.End.invtSubmodule ↑((GeneralLinearGroup.generalLinearEquiv R E) T) ∧
        f.range ∈ Module.End.invtSubmodule ↑((GeneralLinearGroup.generalLinearEquiv R E) T).symm) ∧
      f.ker ∈ Module.End.invtSubmodule ↑((GeneralLinearGroup.generalLinearEquiv R E) T) ∧
        f.ker ∈ Module.End.invtSubmodule ↑((GeneralLinearGroup.generalLinearEquiv R E) T).symm

Tactic:
and_and_and_comm (c := (ker f ∈ _)),

Goal state after:
E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
f : E →ₗ[R] E
hf : IsIdempotentElem f
T : (E →ₗ[R] E)ˣ
⊢ Commute f ↑((GeneralLinearGroup.generalLinearEquiv R E) T) ↔
    (f.range ∈ Module.End.invtSubmodule ↑((GeneralLinearGroup.generalLinearEquiv R E) T) ∧
        f.ker ∈ Module.End.invtSubmodule ↑((GeneralLinearGroup.generalLinearEquiv R E) T)) ∧
      f.range ∈ Module.End.invtSubmodule ↑((GeneralLinearGroup.generalLinearEquiv R E) T).symm ∧
        f.ker ∈ Module.End.invtSubmodule ↑((GeneralLinearGroup.generalLinearEquiv R E) T).symm
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
x : α × α
x✝² x✝¹ x✝ : α
⊢ (x✝², x✝¹) ∈ {x} → (x✝¹, x✝) ∈ {x} → (x✝², x✝) ∈ {x}

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
⊢ graph id = SetRel.id

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
⊢ graph (f ∘ g) = graph g ○ graph f

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
inst✝ : r.IsIrrefl
⊢ ¬{x | x ∈ s}.Nontrivial ↔ {x | x ∈ s}.Subsingleton

Tactic:
Set.not_nontrivial_iff

Goal state after:
α : Type u_1
r : SetRel α α
s : RelSeries r
inst✝ : r.IsIrrefl
⊢ {x | x ∈ s}.Subsingleton ↔ {x | x ∈ s}.Subsingleton
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ≃ β
⊢ Function.graph ⇑f.symm = (Function.graph ⇑f).inv

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
h : ∀ (a : α), ∃! b, (a, b) ∈ R
f : α → β
hf : ∀ (x : α), (x, f x) ∈ R
⊢ ∀ (y : α → β), (fun f ↦ Function.graph f = R) y → y = f

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: case mpr.mp
α : Type u_1
β : Type u_2
R : SetRel α β
h : ∀ (a : α), ∃! b, (a, b) ∈ R
f : α → β
hf : ∀ (x : α), (x, f x) ∈ R
a : α
b : β
⊢ (a, b) ∈ Function.graph f → (a, b) ∈ R

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_3
α : 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 : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑m = ↑i
⊢ m = i.castSucc

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 : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑m = ↑i
⊢ y = a

Tactic:
· ext; exact hm

Goal state after:
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 : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑m = ↑i
⊢ y = a