harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Option/Basic.lean
theorem elim_comp₂ (h : α → β → γ) {f : γ → α} {x : α} {g : γ → β} {y : β}
    {i : Option γ} : (i.elim (h x y) fun j => h (f j) (g j)) = h (i.elim x f) (i.elim y g)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β → γ
f : γ → α
x : α
g : γ → β
y : β
i : Option γ
⊢ (i.elim (h x y) fun j => h (f j) (g j)) = h (i.elim x f) (i.elim y g)

Tactic:
cases i <;> rfl

Result:
no goals
-- Mathlib/Topology/Compactness/Paracompact.lean
theorem precise_refinement [ParacompactSpace X] (u : ι → Set X) (uo : ∀ a, IsOpen (u a))
    (uc : ⋃ i, u i = univ) : ∃ v : ι → Set X, (∀ a, IsOpen (v a)) ∧ ⋃ i, v i = univ ∧
    LocallyFinite v ∧ ∀ a, v a ⊆ u a

Proof state:
case refine_4
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : ⋃ i, u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | (t i ∩ U x).Nonempty}.Finite
⊢ ∀ (a : ι) (x : X), (∃ i, ∃ (_ : ind i = a), x ∈ t i) → x ∈ u a

Tactic:
rintro i x ⟨a, rfl, hxa⟩

Result:
case refine_4.intro.intro
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : ⋃ i, u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | (t i ∩ U x).Nonempty}.Finite
x : X
a : α
hxa : x ∈ t a
⊢ x ∈ u (ind a)
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_add_sinh : cosh x + sinh x = exp x

Proof state:
x : ℝ
⊢ cosh x + sinh x = rexp x

Tactic:
rw [← ofReal_inj]

Result:
x : ℝ
⊢ ↑(cosh x + sinh x) = ↑(rexp x)

Proof state:
x : ℝ
⊢ ↑(cosh x + sinh x) = ↑(rexp x)

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean
theorem alternatingFaceMapComplex_obj_d (X : SimplicialObject C) (n : ℕ) :
    ((alternatingFaceMapComplex C).obj X).d (n + 1) n = AlternatingFaceMapComplex.objD X n

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (ChainComplex.of (fun n => X _⦋n⦌) (AlternatingFaceMapComplex.objD X) ⋯).d (n + 1) n =
    AlternatingFaceMapComplex.objD X n

Tactic:
apply ChainComplex.of_d

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ ((alternatingFaceMapComplex C).obj X).d (n + 1) n = AlternatingFaceMapComplex.objD X n

Tactic:
dsimp only [alternatingFaceMapComplex, AlternatingFaceMapComplex.obj]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (ChainComplex.of (fun n => X _⦋n⦌) (AlternatingFaceMapComplex.objD X) ⋯).d (n + 1) n =
    AlternatingFaceMapComplex.objD X n
-- Mathlib/RingTheory/Polynomial/Quotient.lean
theorem polynomialQuotientEquivQuotientPolynomial_map_mk (I : Ideal R) (f : R[X]) :
    I.polynomialQuotientEquivQuotientPolynomial (f.map <| Quotient.mk I) =
    Quotient.mk (map C I : Ideal R[X]) f

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ I.polynomialQuotientEquivQuotientPolynomial (Polynomial.map (Quotient.mk I) f) = (Quotient.mk (map C I)) f

Tactic:
apply (polynomialQuotientEquivQuotientPolynomial I).symm.injective

Result:
case a
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ I.polynomialQuotientEquivQuotientPolynomial.symm
      (I.polynomialQuotientEquivQuotientPolynomial (Polynomial.map (Quotient.mk I) f)) =
    I.polynomialQuotientEquivQuotientPolynomial.symm ((Quotient.mk (map C I)) f)

Proof state:
case a
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ I.polynomialQuotientEquivQuotientPolynomial.symm
      (I.polynomialQuotientEquivQuotientPolynomial (Polynomial.map (Quotient.mk I) f)) =
    I.polynomialQuotientEquivQuotientPolynomial.symm ((Quotient.mk (map C I)) f)

Tactic:
rw [RingEquiv.symm_apply_apply, polynomialQuotientEquivQuotientPolynomial_symm_mk]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem iSup_ord {ι} {f : ι → Cardinal} (hf : BddAbove (range f)) :
    (iSup f).ord = ⨆ i, (f i).ord

Proof state:
case h.e'_3.h.e'_3
ι : Sort u_4
f : ι → Cardinal.{u_5}
hf : BddAbove (range f)
⊢ (range fun i => (f i).ord) = ord '' range f

Tactic:
conv_lhs => change range (ord ∘ f)

Result:
case h.e'_3.h.e'_3
ι : Sort u_4
f : ι → Cardinal.{u_5}
hf : BddAbove (range f)
⊢ range (ord ∘ f) = ord '' range f

Proof state:
case h.e'_3.h.e'_3
ι : Sort u_4
f : ι → Cardinal.{u_5}
hf : BddAbove (range f)
⊢ range (ord ∘ f) = ord '' range f

Tactic:
rw [range_comp]

Result:
no goals

Proof state:
ι : Sort u_4
f : ι → Cardinal.{u_5}
hf : BddAbove (range f)
⊢ (iSup f).ord = ⨆ i, (f i).ord

Tactic:
unfold iSup

Result:
ι : Sort u_4
f : ι → Cardinal.{u_5}
hf : BddAbove (range f)
⊢ (sSup (range f)).ord = sSup (range fun i => (f i).ord)

Proof state:
ι : Sort u_4
f : ι → Cardinal.{u_5}
hf : BddAbove (range f)
⊢ (sSup (range f)).ord = sSup (range fun i => (f i).ord)

Tactic:
convert sSup_ord hf

Result:
case h.e'_3.h.e'_3
ι : Sort u_4
f : ι → Cardinal.{u_5}
hf : BddAbove (range f)
⊢ (range fun i => (f i).ord) = ord '' range f
-- Mathlib/Probability/Independence/Kernel.lean
@[simp] lemma indepSet_zero_left {s t : Set Ω} : IndepSet s t (0 : Kernel α Ω) μ

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
s t : Set Ω
⊢ IndepSet s t 0 μ

Tactic:
simp [IndepSet]

Result:
no goals
-- Mathlib/Algebra/Order/AddTorsor.lean
theorem smul_lt_smul_of_lt_of_le [Preorder G] [Preorder P] [SMul G P] [IsOrderedCancelSMul G P]
    {a b : G} {c d : P} (h₁ : a < b) (h₂ : c ≤ d) : a • c < b • d

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : Preorder G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
⊢ ¬b • d ≤ a • d

Tactic:
by_contra hbad

Result:
G : Type u_1
P : Type u_2
inst✝³ : Preorder G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
hbad : b • d ≤ a • d
⊢ False

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : Preorder G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b ∧ ¬b ≤ a
h₂ : c ≤ d
hbad : b • d ≤ a • d
h : b ≤ a
⊢ False

Tactic:
simp_all only [not_true_eq_false, and_false]

Result:
no goals

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : Preorder G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
hbad : b • d ≤ a • d
⊢ False

Tactic:
have h : b ≤ a := IsOrderedCancelSMul.le_of_smul_le_smul_right b a d hbad

Result:
G : Type u_1
P : Type u_2
inst✝³ : Preorder G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
hbad : b • d ≤ a • d
h : b ≤ a
⊢ False

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : Preorder G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
⊢ a • d < b • d

Tactic:
refine lt_of_le_not_le (IsOrderedSMul.smul_le_smul_right a b (le_of_lt h₁) d) ?_

Result:
G : Type u_1
P : Type u_2
inst✝³ : Preorder G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
⊢ ¬b • d ≤ a • d

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : Preorder G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
hbad : b • d ≤ a • d
h : b ≤ a
⊢ False

Tactic:
rw [@lt_iff_le_not_le] at h₁

Result:
G : Type u_1
P : Type u_2
inst✝³ : Preorder G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b ∧ ¬b ≤ a
h₂ : c ≤ d
hbad : b • d ≤ a • d
h : b ≤ a
⊢ False

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : Preorder G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
⊢ a • c < b • d

Tactic:
refine lt_of_le_of_lt (IsOrderedSMul.smul_le_smul_left c d h₂ a) ?_

Result:
G : Type u_1
P : Type u_2
inst✝³ : Preorder G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
⊢ a • d < b • d
-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem Fix.rec_eq {α : Type _} (g : F α → α) (x : F (Fix F)) :
    Fix.rec g (Fix.mk x) = g (Fix.rec g <$> x)

Proof state:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
⊢ rec g (mk x) = g (rec g <$> x)

Tactic:
conv =>
  lhs
  rw [Fix.rec, Fix.mk]
  dsimp

Result:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
⊢ recF g (PFunctor.W.mk ((P F).map fixToW (repr x))) = g (rec g <$> x)

Proof state:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
⊢ recF g ∘ fixToW = rec g

Tactic:
ext ⟨x⟩

Result:
case h.mk
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x✝¹ : F (Fix F)
x✝ : Fix F
x : (P F).W
⊢ (recF g ∘ fixToW) (Quot.mk (⇑Wsetoid) x) = rec g (Quot.mk (⇑Wsetoid) x)

Proof state:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
⊢ rec g (mk x) = g (rec g <$> x)

Tactic:
have : recF g ∘ fixToW = Fix.rec g := by
  ext ⟨x⟩
  apply recF_eq_of_Wequiv
  rw [fixToW]
  apply Wrepr_equiv

Result:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
⊢ rec g (mk x) = g (rec g <$> x)

Proof state:
case h.mk.a
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x✝¹ : F (Fix F)
x✝ : Fix F
x : (P F).W
⊢ Wequiv (Quotient.lift Wrepr ⋯ (Quot.mk (⇑Wsetoid) x)) x

Tactic:
apply Wrepr_equiv

Result:
no goals

Proof state:
case h.mk
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x✝¹ : F (Fix F)
x✝ : Fix F
x : (P F).W
⊢ (recF g ∘ fixToW) (Quot.mk (⇑Wsetoid) x) = rec g (Quot.mk (⇑Wsetoid) x)

Tactic:
apply recF_eq_of_Wequiv

Result:
case h.mk.a
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x✝¹ : F (Fix F)
x✝ : Fix F
x : (P F).W
⊢ Wequiv (fixToW (Quot.mk (⇑Wsetoid) x)) x

Proof state:
case mk
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : (P F).B a → Fix F
h : repr x = ⟨a, f⟩
⊢ recF g (PFunctor.W.mk ((P F).map fixToW ⟨a, f⟩)) = g (rec g <$> x)

Tactic:
rw [PFunctor.map_eq, recF_eq, ← PFunctor.map_eq, PFunctor.W.dest_mk, PFunctor.map_map, abs_map,
  ← h, abs_repr, this]

Result:
no goals

Proof state:
case h.mk.a
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x✝¹ : F (Fix F)
x✝ : Fix F
x : (P F).W
⊢ Wequiv (fixToW (Quot.mk (⇑Wsetoid) x)) x

Tactic:
rw [fixToW]

Result:
case h.mk.a
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x✝¹ : F (Fix F)
x✝ : Fix F
x : (P F).W
⊢ Wequiv (Quotient.lift Wrepr ⋯ (Quot.mk (⇑Wsetoid) x)) x

Proof state:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
⊢ recF g (PFunctor.W.mk ((P F).map fixToW (repr x))) = g (rec g <$> x)

Tactic:
rcases h : repr x with ⟨a, f⟩

Result:
case mk
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : (P F).B a → Fix F
h : repr x = ⟨a, f⟩
⊢ recF g (PFunctor.W.mk ((P F).map fixToW ⟨a, f⟩)) = g (rec g <$> x)
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExtClass.lean
@[simp]
lemma comp_extClass : (Ext.mk₀ S.g).comp hS.extClass (zero_add 1) = 0

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (singleFunctor C 0).map S.g ≫ hS.singleδ = 0

Tactic:
exact comp_distTriang_mor_zero₂₃ _ hS.singleTriangle_distinguished

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (Ext.mk₀ S.g).comp hS.extClass ⋯ = 0

Tactic:
ext

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ ((Ext.mk₀ S.g).comp hS.extClass ⋯).hom = Ext.hom 0

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ ((Ext.mk₀ S.g).comp hS.extClass ⋯).hom = Ext.hom 0

Tactic:
simp only [Ext.comp_hom, Ext.mk₀_hom, extClass_hom, Ext.zero_hom,
  ShiftedHom.mk₀_comp]

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (singleFunctor C 0).map S.g ≫ hS.singleδ = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
⊢ (Ext.mk₀ S.g).comp hS.extClass ⋯ = 0

Tactic:
letI := HasDerivedCategory.standard C

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (Ext.mk₀ S.g).comp hS.extClass ⋯ = 0
-- Mathlib/LinearAlgebra/TensorProduct/Basis.lean
theorem Basis.tensorProduct_apply (b : Basis ι S M) (c : Basis κ R N) (i : ι) (j : κ) :
    Basis.tensorProduct b c (i, j) = b i ⊗ₜ c j

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring S
inst✝⁶ : Algebra R S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
b : Basis ι S M
c : Basis κ R N
i : ι
j : κ
⊢ (b.tensorProduct c) (i, j) = b i ⊗ₜ[R] c j

Tactic:
simp [Basis.tensorProduct]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/AC.lean
theorem Context.eq_of_norm (ctx : Context α) (a b : Expr) (h : norm ctx a == norm ctx b) : eval α ctx a = eval α ctx b

Proof state:
α : Sort u_1
ctx : Context α
a b : Expr
h : (norm ctx a == norm ctx b) = true
⊢ eval α ctx a = eval α ctx b

Tactic:
have h := congrArg (evalList α ctx) (eq_of_beq h)

Result:
α : Sort u_1
ctx : Context α
a b : Expr
h✝ : (norm ctx a == norm ctx b) = true
h : evalList α ctx (norm ctx a) = evalList α ctx (norm ctx b)
⊢ eval α ctx a = eval α ctx b

Proof state:
α : Sort u_1
ctx : Context α
a b : Expr
h✝ : (norm ctx a == norm ctx b) = true
h : eval α ctx a = eval α ctx b
⊢ eval α ctx a = eval α ctx b

Tactic:
assumption

Result:
no goals

Proof state:
α : Sort u_1
ctx : Context α
a b : Expr
h✝ : (norm ctx a == norm ctx b) = true
h : evalList α ctx (norm ctx a) = evalList α ctx (norm ctx b)
⊢ eval α ctx a = eval α ctx b

Tactic:
rw [eval_norm, eval_norm] at h

Result:
α : Sort u_1
ctx : Context α
a b : Expr
h✝ : (norm ctx a == norm ctx b) = true
h : eval α ctx a = eval α ctx b
⊢ eval α ctx a = eval α ctx b
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem mem_factors_iff_dvd {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) :
    Associates.mk p ∈ factors (Associates.mk a) ↔ p ∣ a

Proof state:
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ Associates.mk p ∈ (Associates.mk a).factors → p ∣ a

Tactic:
rw [← mk_dvd_mk]

Result:
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ Associates.mk p ∈ (Associates.mk a).factors → Associates.mk p ∣ Associates.mk a

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ Associates.mk p ∈ (Associates.mk a).factors ↔ p ∣ a

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ Associates.mk p ∈ (Associates.mk a).factors → p ∣ a

case mpr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ p ∣ a → Associates.mk p ∈ (Associates.mk a).factors

Proof state:
case mpr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ p ∣ a → Associates.mk p ∈ (Associates.mk a).factors

Tactic:
apply mem_factors_of_dvd ha0 hp

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ Associates.mk p ∈ (Associates.mk a).factors → Associates.mk p ∣ Associates.mk a

Tactic:
apply dvd_of_mem_factors

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/RankAndCardinality.lean
theorem IntermediateField.rank_sup_le
    {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) :
    Module.rank F ↥(A ⊔ B) ≤ Module.rank F A * Module.rank F B

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B

Tactic:
by_cases hA : Algebra.IsAlgebraic F A

Result:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
hA : Algebra.IsAlgebraic F ↥A
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B

case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
hA : ¬Algebra.IsAlgebraic F ↥A
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B

Proof state:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
hA : ¬Algebra.IsAlgebraic F ↥A
hB : Algebra.IsAlgebraic F ↥B
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B

Tactic:
exact rank_sup_le_of_isAlgebraic A B (Or.inr hB)

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental F ↥A
hB : Algebra.Transcendental F ↥B
this✝¹ : Algebra.Transcendental F ↥(A ⊔ B)
this✝ : Infinite ↥A
this : Infinite ↥B
⊢ Cardinal.lift.{v, u} #F ⊔ Cardinal.lift.{u, v} #↑(↑A ∪ ↑B) ⊔ ℵ₀ ≤
    Cardinal.lift.{v, u} #F ⊔ Cardinal.lift.{u, v} (#↥A ⊔ #↥B) ⊔ ℵ₀

Tactic:
gcongr

Result:
case h₁.h₁
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental F ↥A
hB : Algebra.Transcendental F ↥B
this✝¹ : Algebra.Transcendental F ↥(A ⊔ B)
this✝ : Infinite ↥A
this : Infinite ↥B
⊢ Cardinal.lift.{u, v} #↑(↑A ∪ ↑B) ≤ Cardinal.lift.{u, v} (#↥A ⊔ #↥B)

Proof state:
case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental F ↥A
hB : Algebra.Transcendental F ↥B
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B

Tactic:
haveI : Algebra.Transcendental F ↥(A ⊔ B) := .ringHom_of_comp_eq (RingHom.id F)
  (inclusion le_sup_left) Function.surjective_id (inclusion_injective _) rfl

Result:
case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental F ↥A
hB : Algebra.Transcendental F ↥B
this : Algebra.Transcendental F ↥(A ⊔ B)
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B
-- Mathlib/Data/Set/Image.lean
theorem image_empty (f : α → β) : f '' ∅ = ∅

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
x✝ : β
⊢ x✝ ∈ f '' ∅ ↔ x✝ ∈ ∅

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ f '' ∅ = ∅

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
x✝ : β
⊢ x✝ ∈ f '' ∅ ↔ x✝ ∈ ∅
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_ofZNum [AddGroupWithOne α] (n : ZNum) : (ofZNum n : α) = Int.toNat n

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ ↑(ofZNum n) = ↑(↑n).toNat

Tactic:
rw [← cast_to_nat, ofZNum_toNat]

Result:
no goals
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem sq_ne_two_fin_zmod_four (z : ZMod 4) : z * z ≠ 2

Proof state:
z : Fin 4
⊢ z * z ≠ 2

Tactic:
fin_cases z <;> decide

Result:
no goals

Proof state:
z : ZMod 4
⊢ z * z ≠ 2

Tactic:
change Fin 4 at z

Result:
z : Fin 4
⊢ z * z ≠ 2
-- Mathlib/Order/Interval/Multiset.lean
theorem Ioo_self : Ioo a a = 0

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Ioo a a = 0

Tactic:
rw [Ioo, Finset.Ioo_self, Finset.empty_val]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Fold.lean
theorem dfoldrM_eq_foldrM [Monad m] [LawfulMonad m] (f : (i : Fin n) → α → m α) (x) :
    dfoldrM n (fun _ => α) f x = foldrM n f x

Proof state:
m : Type u_1 → Type u_2
n : Nat
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin n → α → m α
x : (fun x => α) (last n)
⊢ dfoldrM n (fun x => α) f x = foldrM n f x

Tactic:
induction n with
| zero => simp only [dfoldrM_zero, foldrM_zero]
| succ n ih => simp only [dfoldrM_succ, foldrM_succ, Function.comp_def, ih]

Result:
no goals

Proof state:
case zero
m : Type u_1 → Type u_2
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin 0 → α → m α
x : α
⊢ dfoldrM 0 (fun x => α) f x = foldrM 0 f x

Tactic:
simp only [dfoldrM_zero, foldrM_zero]

Result:
no goals

Proof state:
case succ
m : Type u_1 → Type u_2
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : Nat
ih : ∀ (f : Fin n → α → m α) (x : α), dfoldrM n (fun x => α) f x = foldrM n f x
f : Fin (n + 1) → α → m α
x : α
⊢ dfoldrM (n + 1) (fun x => α) f x = foldrM (n + 1) f x

Tactic:
simp only [dfoldrM_succ, foldrM_succ, Function.comp_def, ih]

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem AlgebraicIndependent.to_subtype_range {ι} {f : ι → A} (hf : AlgebraicIndependent R f) :
    AlgebraicIndependent R ((↑) : range f → A)

Proof state:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι : Type u_7
f : ι → A
hf : AlgebraicIndependent R f
⊢ AlgebraicIndependent R Subtype.val

Tactic:
nontriviality R

Result:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι : Type u_7
f : ι → A
hf : AlgebraicIndependent R f
a✝ : Nontrivial R
⊢ AlgebraicIndependent R Subtype.val

Proof state:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι : Type u_7
f : ι → A
hf : AlgebraicIndependent R f
a✝ : Nontrivial R
⊢ AlgebraicIndependent R Subtype.val

Tactic:
rwa [algebraicIndependent_subtype_range hf.injective]

Result:
no goals