harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/End.lean
theorem sumCongrHom_injective {α β : Type*} : Function.Injective (sumCongrHom α β)

Proof state:
case mk.mk
α : Type u_6
β : Type u_7
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)

Tactic:
rw [Prod.mk.inj_iff]

Result:
case mk.mk
α : Type u_6
β : Type u_7
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝

Proof state:
case mk.mk.left.H
α : Type u_6
β : Type u_7
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
i : α
⊢ fst✝¹ i = fst✝ i

Tactic:
simpa using Equiv.congr_fun h (Sum.inl i)

Result:
no goals

Proof state:
case mk.mk
α : Type u_6
β : Type u_7
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝

Tactic:
constructor <;> ext i

Result:
case mk.mk.left.H
α : Type u_6
β : Type u_7
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
i : α
⊢ fst✝¹ i = fst✝ i

case mk.mk.right.H
α : Type u_6
β : Type u_7
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
i : β
⊢ snd✝¹ i = snd✝ i

Proof state:
α : Type u_6
β : Type u_7
⊢ Function.Injective ⇑(sumCongrHom α β)

Tactic:
rintro ⟨⟩ ⟨⟩ h

Result:
case mk.mk
α : Type u_6
β : Type u_7
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)

Proof state:
case mk.mk.right.H
α : Type u_6
β : Type u_7
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
i : β
⊢ snd✝¹ i = snd✝ i

Tactic:
simpa using Equiv.congr_fun h (Sum.inr i)

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/BigOperators.lean
lemma multiSetProd_mem {ι : Type*} (s : Multiset ι) (f : ι → R) (hs : ∃ x ∈ s, f x ∈ I) :
    (s.map f).prod ∈ I

Proof state:
case mk
R : Type u_1
inst✝ : CommRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
a✝ : List ι
hs : ∃ x ∈ Quot.mk (⇑(List.isSetoid ι)) a✝, f x ∈ I
⊢ (Multiset.map f (Quot.mk (⇑(List.isSetoid ι)) a✝)).prod ∈ I

Tactic:
simpa using listProd_mem (hl := hs)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∃ x ∈ s, f x ∈ I
⊢ (Multiset.map f s).prod ∈ I

Tactic:
rcases s

Result:
case mk
R : Type u_1
inst✝ : CommRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
a✝ : List ι
hs : ∃ x ∈ Quot.mk (⇑(List.isSetoid ι)) a✝, f x ∈ I
⊢ (Multiset.map f (Quot.mk (⇑(List.isSetoid ι)) a✝)).prod ∈ I
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_hom (f : β₁ → β₂) (g₁ : α → β₁ → β₁) (g₂ : α → β₂ → β₂) (l : Array α) (init : β₁)
    (H : ∀ x y, g₂ x (f y) = f (g₁ x y)) : l.foldr g₂ (f init) = f (l.foldr g₁ init)

Proof state:
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
f : β₁ → β₂
g₁ : α → β₁ → β₁
g₂ : α → β₂ → β₂
l : Array α
init : β₁
H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)
⊢ foldr g₂ (f init) l = f (foldr g₁ init l)

Tactic:
cases l

Result:
case mk
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
f : β₁ → β₂
g₁ : α → β₁ → β₁
g₂ : α → β₂ → β₂
init : β₁
H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)
toList✝ : List α
⊢ foldr g₂ (f init) { toList := toList✝ } = f (foldr g₁ init { toList := toList✝ })

Proof state:
case mk
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
f : β₁ → β₂
g₁ : α → β₁ → β₁
g₂ : α → β₂ → β₂
init : β₁
H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)
toList✝ : List α
⊢ List.foldr g₂ (f init) toList✝ = f (List.foldr g₁ init toList✝)

Tactic:
rw [List.foldr_hom _ _ _ _ _ H]

Result:
no goals

Proof state:
case mk
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
f : β₁ → β₂
g₁ : α → β₁ → β₁
g₂ : α → β₂ → β₂
init : β₁
H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)
toList✝ : List α
⊢ foldr g₂ (f init) { toList := toList✝ } = f (foldr g₁ init { toList := toList✝ })

Tactic:
simp

Result:
case mk
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
f : β₁ → β₂
g₁ : α → β₁ → β₁
g₂ : α → β₂ → β₂
init : β₁
H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)
toList✝ : List α
⊢ List.foldr g₂ (f init) toList✝ = f (List.foldr g₁ init toList✝)
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma HasFPowerSeriesAt.pi
    (hf : ∀ i, HasFPowerSeriesAt (f i) (p i) e) :
    HasFPowerSeriesAt (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) e

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesAt (f i) (p i) e
⊢ HasFPowerSeriesAt (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) e

Tactic:
simp_rw [← hasFPowerSeriesWithinAt_univ] at hf ⊢

Result:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) Set.univ e
⊢ HasFPowerSeriesWithinAt (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) Set.univ e

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) Set.univ e
⊢ HasFPowerSeriesWithinAt (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) Set.univ e

Tactic:
exact HasFPowerSeriesWithinAt.pi hf

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
lemma List.iSup_mem_map_of_ne_nil {l : List ι} (f : ι → α) (h : l ≠ []) :
    ⨆ x ∈ l, f x ∈ l.map f :=
  l.iSup_mem_map_of_exists_sSup_empty_le _ (by simpa using exists_mem_of_ne_nil _ h)

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
l : List ι
f : ι → α
h : l ≠ []
⊢ ∃ x ∈ l, sSup ∅ ≤ f x

Tactic:
simpa using exists_mem_of_ne_nil _ h

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem FiniteMultiplicity.or_of_add {p a b : α} (hf : FiniteMultiplicity p (a + b)) :
    FiniteMultiplicity p a ∨ FiniteMultiplicity p b

Proof state:
α : Type u_1
inst✝ : Semiring α
p a b : α
hf : FiniteMultiplicity p (a + b)
⊢ FiniteMultiplicity p a ∨ FiniteMultiplicity p b

Tactic:
by_contra! nh

Result:
α : Type u_1
inst✝ : Semiring α
p a b : α
hf : FiniteMultiplicity p (a + b)
nh : ¬FiniteMultiplicity p a ∧ ¬FiniteMultiplicity p b
⊢ False

Proof state:
α : Type u_1
inst✝ : Semiring α
p a b : α
hf : FiniteMultiplicity p (a + b)
nh : ¬FiniteMultiplicity p a ∧ ¬FiniteMultiplicity p b
⊢ False

Tactic:
obtain ⟨c, hc⟩ := hf

Result:
case intro
α : Type u_1
inst✝ : Semiring α
p a b : α
nh : ¬FiniteMultiplicity p a ∧ ¬FiniteMultiplicity p b
c : ℕ
hc : ¬p ^ (c + 1) ∣ a + b
⊢ False

Proof state:
case intro
α : Type u_1
inst✝ : Semiring α
p a b : α
nh : ¬FiniteMultiplicity p a ∧ ¬FiniteMultiplicity p b
c : ℕ
hc : ¬p ^ (c + 1) ∣ a + b
⊢ False

Tactic:
simp_all [dvd_add]

Result:
no goals
-- Mathlib/Topology/Algebra/MulAction.lean
theorem MulAction.continuousSMul_compHom
    {N : Type*} [TopologicalSpace N] [Monoid N] {f : N →* M} (hf : Continuous f) :
    letI : MulAction N X := MulAction.compHom _ f
    ContinuousSMul N X

Proof state:
M : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace X
inst✝⁴ : Monoid M
inst✝³ : MulAction M X
inst✝² : ContinuousSMul M X
N : Type u_5
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : N →* M
hf : Continuous ⇑f
⊢ ContinuousSMul N X

Tactic:
let _ : MulAction N X := MulAction.compHom _ f

Result:
M : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace X
inst✝⁴ : Monoid M
inst✝³ : MulAction M X
inst✝² : ContinuousSMul M X
N : Type u_5
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : N →* M
hf : Continuous ⇑f
x✝ : MulAction N X := compHom X f
⊢ ContinuousSMul N X

Proof state:
M : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace X
inst✝⁴ : Monoid M
inst✝³ : MulAction M X
inst✝² : ContinuousSMul M X
N : Type u_5
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : N →* M
hf : Continuous ⇑f
x✝ : MulAction N X := compHom X f
⊢ ContinuousSMul N X

Tactic:
exact ⟨(hf.comp continuous_fst).smul continuous_snd⟩

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Boundary.lean
lemma not_boundaryLE_prev [e.IsRelIff] {i j : ι} (hi : c.Rel i j) :
    ¬ e.BoundaryLE i

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hi : c.Rel i j
⊢ ¬e.BoundaryLE i

Tactic:
dsimp [BoundaryLE]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hi : c.Rel i j
⊢ ¬(c'.Rel (e.f i) (c'.next (e.f i)) ∧ ∀ (k : ι), ¬c'.Rel (e.f i) (e.f k))

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hi : c.Rel i j
a✝ : c'.Rel (e.f i) (c'.next (e.f i))
⊢ ∃ x, c'.Rel (e.f i) (e.f x)

Tactic:
exact ⟨j, by simpa only [e.rel_iff] using hi⟩

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hi : c.Rel i j
a✝ : c'.Rel (e.f i) (c'.next (e.f i))
⊢ c'.Rel (e.f i) (e.f j)

Tactic:
simpa only [e.rel_iff] using hi

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hi : c.Rel i j
⊢ c'.Rel (e.f i) (c'.next (e.f i)) → ∃ x, c'.Rel (e.f i) (e.f x)

Tactic:
intro

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hi : c.Rel i j
a✝ : c'.Rel (e.f i) (c'.next (e.f i))
⊢ ∃ x, c'.Rel (e.f i) (e.f x)

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hi : c.Rel i j
⊢ ¬(c'.Rel (e.f i) (c'.next (e.f i)) ∧ ∀ (k : ι), ¬c'.Rel (e.f i) (e.f k))

Tactic:
simp only [not_and, not_forall, not_not]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hi : c.Rel i j
⊢ c'.Rel (e.f i) (c'.next (e.f i)) → ∃ x, c'.Rel (e.f i) (e.f x)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/RelabelFin.lean
theorem of_maxLiteral_eq_none (f : CNF Nat) (h : f.maxLiteral = none) :
    ∀ lit, ¬Mem lit f

Proof state:
case intro.intro
f : CNF Nat
lit : Nat
h : List.filterMap Clause.maxLiteral f = []
clause : Clause Nat
hclause1 : clause ∈ f
hclause2 : Clause.Mem lit clause
⊢ False

Tactic:
have := Clause.of_maxLiteral_eq_none clause (List.forall_none_of_filterMap_eq_nil h clause hclause1) lit

Result:
case intro.intro
f : CNF Nat
lit : Nat
h : List.filterMap Clause.maxLiteral f = []
clause : Clause Nat
hclause1 : clause ∈ f
hclause2 : Clause.Mem lit clause
this : ¬Clause.Mem lit clause
⊢ False

Proof state:
case intro.intro
f : CNF Nat
lit : Nat
h : List.filterMap Clause.maxLiteral f = []
clause : Clause Nat
hclause1 : clause ∈ f
hclause2 : Clause.Mem lit clause
this : ¬Clause.Mem lit clause
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
f : CNF Nat
h : f.maxLiteral = none
lit : Nat
hlit : Mem lit f
⊢ False

Tactic:
simp only [maxLiteral, List.max?_eq_none_iff] at h

Result:
f : CNF Nat
lit : Nat
hlit : Mem lit f
h : List.filterMap Clause.maxLiteral f = []
⊢ False

Proof state:
f : CNF Nat
lit : Nat
hlit : Mem lit f
h : List.filterMap Clause.maxLiteral f = []
⊢ False

Tactic:
dsimp [Mem] at hlit

Result:
f : CNF Nat
lit : Nat
hlit : ∃ c, c ∈ f ∧ Clause.Mem lit c
h : List.filterMap Clause.maxLiteral f = []
⊢ False

Proof state:
f : CNF Nat
lit : Nat
hlit : ∃ c, c ∈ f ∧ Clause.Mem lit c
h : List.filterMap Clause.maxLiteral f = []
⊢ False

Tactic:
rcases hlit with ⟨clause, ⟨hclause1, hclause2⟩⟩

Result:
case intro.intro
f : CNF Nat
lit : Nat
h : List.filterMap Clause.maxLiteral f = []
clause : Clause Nat
hclause1 : clause ∈ f
hclause2 : Clause.Mem lit clause
⊢ False

Proof state:
f : CNF Nat
h : f.maxLiteral = none
⊢ ∀ (lit : Nat), ¬Mem lit f

Tactic:
intro lit hlit

Result:
f : CNF Nat
h : f.maxLiteral = none
lit : Nat
hlit : Mem lit f
⊢ False
-- Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
theorem coeff_fslope : p.fslope.coeff n = p.coeff (n + 1)

Proof state:
𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
⊢ p.fslope.coeff n = p.coeff (n + 1)

Tactic:
simp only [fslope, coeff, ContinuousMultilinearMap.curryLeft_apply]

Result:
𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
⊢ (p (n + 1)) (cons 1 1) = (p (n + 1)) 1

Proof state:
case h.e_6.h
𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
⊢ cons 1 1 = 1

Tactic:
exact Fin.cons_self_tail (fun _ => (1 : 𝕜))

Result:
no goals

Proof state:
𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
⊢ (p (n + 1)) (cons 1 1) = (p (n + 1)) 1

Tactic:
congr 1

Result:
case h.e_6.h
𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
⊢ cons 1 1 = 1
-- Mathlib/CategoryTheory/Limits/Constructions/Filtered.lean
theorem hasCoproducts_of_finite_and_filtered [HasFiniteCoproducts C]
    [HasFilteredColimitsOfSize.{w, w} C] : HasCoproducts.{w} C := fun α => by
  classical exact ⟨fun F => HasColimit.mk (liftToFinsetColimitCocone F)⟩

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
α : Type w
⊢ HasColimitsOfShape (Discrete α) C

Tactic:
exact ⟨fun F => HasColimit.mk (liftToFinsetColimitCocone F)⟩

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
α : Type w
⊢ HasColimitsOfShape (Discrete α) C

Tactic:
classical exact ⟨fun F => HasColimit.mk (liftToFinsetColimitCocone F)⟩

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
@[simp high]
lemma swap_mem_divisorsAntidiag : xy.swap ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag

Proof state:
xy : ℤ × ℤ
z : ℤ
⊢ xy.swap ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag

Tactic:
simp [mul_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean
theorem exists_finite_submodule_of_finite (s : Set (M ⊗[R] N)) (hs : s.Finite) :
    ∃ (M' : Submodule R M) (N' : Submodule R N), Module.Finite R M' ∧ Module.Finite R N' ∧
      s ⊆ LinearMap.range (mapIncl M' N')

Proof state:
case intro.intro.intro.intro.refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s✝ : Set (M ⊗[R] N)
hs : s✝.Finite
a : M ⊗[R] N
s : Set (M ⊗[R] N)
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))
x : M
y : N
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ insert (x ⊗ₜ[R] y) s ⊆ ↑(LinearMap.range (mapIncl M' N'))

Tactic:
refine ⟨_, _, hM'.sup (fg_span_singleton x),
  hN'.sup (fg_span_singleton y), Set.insert_subset ?_ fun z hz ↦ ?_⟩

Result:
case intro.intro.intro.intro.refine_2.refine_1
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s✝ : Set (M ⊗[R] N)
hs : s✝.Finite
a : M ⊗[R] N
s : Set (M ⊗[R] N)
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))
x : M
y : N
⊢ x ⊗ₜ[R] y ∈ ↑(LinearMap.range (mapIncl (M' ⊔ span R {x}) (N' ⊔ span R {y})))

case intro.intro.intro.intro.refine_2.refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s✝ : Set (M ⊗[R] N)
hs : s✝.Finite
a : M ⊗[R] N
s : Set (M ⊗[R] N)
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))
x : M
y : N
z : M ⊗[R] N
hz : z ∈ s
⊢ z ∈ ↑(LinearMap.range (mapIncl (M' ⊔ span R {x}) (N' ⊔ span R {y})))
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem algebraicIndependent_iUnion_of_directed {η : Type*} [Nonempty η] {s : η → Set A}
    (hs : Directed (· ⊆ ·) s) (h : ∀ i, AlgebraicIndependent R ((↑) : s i → A)) :
    AlgebraicIndependent R ((↑) : (⋃ i, s i) → A)

Proof state:
R : Type u_3
A : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
η : Type u_7
inst✝ : Nonempty η
s : η → Set A
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), AlgebraicIndependent R Subtype.val
⊢ AlgebraicIndependent R Subtype.val

Tactic:
refine algebraicIndependent_of_finite (⋃ i, s i) fun t ht ft => ?_

Result:
R : Type u_3
A : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
η : Type u_7
inst✝ : Nonempty η
s : η → Set A
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), AlgebraicIndependent R Subtype.val
t : Set A
ht : t ⊆ ⋃ i, s i
ft : t.Finite
⊢ AlgebraicIndependent R Subtype.val

Proof state:
case intro.intro
R : Type u_3
A : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
η : Type u_7
inst✝ : Nonempty η
s : η → Set A
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), AlgebraicIndependent R Subtype.val
t : Set A
ht : t ⊆ ⋃ i, s i
ft : t.Finite
I : Set η
fi : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
⊢ AlgebraicIndependent R Subtype.val

Tactic:
rcases hs.finset_le fi.toFinset with ⟨i, hi⟩

Result:
case intro.intro.intro
R : Type u_3
A : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
η : Type u_7
inst✝ : Nonempty η
s : η → Set A
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), AlgebraicIndependent R Subtype.val
t : Set A
ht : t ⊆ ⋃ i, s i
ft : t.Finite
I : Set η
fi : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
i : η
hi : ∀ i_1 ∈ fi.toFinset, s i_1 ⊆ s i
⊢ AlgebraicIndependent R Subtype.val

Proof state:
case intro.intro.intro
R : Type u_3
A : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
η : Type u_7
inst✝ : Nonempty η
s : η → Set A
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), AlgebraicIndependent R Subtype.val
t : Set A
ht : t ⊆ ⋃ i, s i
ft : t.Finite
I : Set η
fi : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
i : η
hi : ∀ i_1 ∈ fi.toFinset, s i_1 ⊆ s i
⊢ AlgebraicIndependent R Subtype.val

Tactic:
exact (h i).mono (Subset.trans hI <| iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj))

Result:
no goals

Proof state:
R : Type u_3
A : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
η : Type u_7
inst✝ : Nonempty η
s : η → Set A
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), AlgebraicIndependent R Subtype.val
t : Set A
ht : t ⊆ ⋃ i, s i
ft : t.Finite
⊢ AlgebraicIndependent R Subtype.val

Tactic:
rcases finite_subset_iUnion ft ht with ⟨I, fi, hI⟩

Result:
case intro.intro
R : Type u_3
A : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
η : Type u_7
inst✝ : Nonempty η
s : η → Set A
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), AlgebraicIndependent R Subtype.val
t : Set A
ht : t ⊆ ⋃ i, s i
ft : t.Finite
I : Set η
fi : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
⊢ AlgebraicIndependent R Subtype.val
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem cons_self_tail : cons (q 0) (tail q) = q

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ cons (q 0) (tail q) j = q j

Tactic:
rw [← this]

Result:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ cons (q 0) (tail q) j'.succ = q j'.succ

Proof state:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : j = 0
⊢ cons (q 0) (tail q) 0 = q 0

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
⊢ cons (q 0) (tail q) = q

Tactic:
ext j

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
⊢ cons (q 0) (tail q) j = q j

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : ¬j = 0
⊢ cons (q 0) (tail q) j = q j

Tactic:
let j' := pred j h

Result:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
⊢ cons (q 0) (tail q) j = q j

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ cons (q 0) (fun i => q i.succ) j'.succ = q j'.succ

Tactic:
rw [cons_succ]

Result:
no goals

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
⊢ cons (q 0) (tail q) j = q j

Tactic:
by_cases h : j = 0

Result:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : j = 0
⊢ cons (q 0) (tail q) j = q j

case neg
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : ¬j = 0
⊢ cons (q 0) (tail q) j = q j

Proof state:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : j = 0
⊢ cons (q 0) (tail q) j = q j

Tactic:
rw [h]

Result:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : j = 0
⊢ cons (q 0) (tail q) 0 = q 0

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ cons (q 0) (tail q) j'.succ = q j'.succ

Tactic:
unfold tail

Result:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ cons (q 0) (fun i => q i.succ) j'.succ = q j'.succ

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
⊢ cons (q 0) (tail q) j = q j

Tactic:
have : j'.succ = j := succ_pred j h

Result:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ cons (q 0) (tail q) j = q j