harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Perm/DomMulAct.lean
theorem stabilizer_card [DecidableEq α] [DecidableEq ι] [Fintype ι] :
    Fintype.card {g : Perm α // f ∘ g = f} = ∏ i, (Fintype.card {a // f a = i})!

Proof state:
α : Type u_1
ι : Type u_2
f : α → ι
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
x✝ : i ∈ Finset.univ
⊢ Nat.card (Perm { a // f a = i }) = (Fintype.card { a // f a = i })!

Tactic:
rw [Nat.card_eq_fintype_card, Fintype.card_perm]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
f : α → ι
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝ : Perm α
⊢ f ∘ ⇑x✝ = f ↔ mk x✝ ∈ stabilizer (Perm α)ᵈᵐᵃ f

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
f : α → ι
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ Fintype.card { g // f ∘ ⇑g = f } = ∏ i : ι, (Fintype.card { a // f a = i })!

Tactic:
rw [← Nat.card_eq_fintype_card,
  Nat.card_congr (subtypeEquiv mk fun _ ↦ ?_),
  Nat.card_congr MulOpposite.opEquiv,
  Nat.card_congr (DomMulAct.stabilizerMulEquiv f).toEquiv, Nat.card_pi]

Result:
α : Type u_1
ι : Type u_2
f : α → ι
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ ∏ a : ι, Nat.card (Perm { a_1 // f a_1 = a }) = ∏ i : ι, (Fintype.card { a // f a = i })!

α : Type u_1
ι : Type u_2
f : α → ι
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝ : Perm α
⊢ f ∘ ⇑x✝ = f ↔ mk x✝ ∈ stabilizer (Perm α)ᵈᵐᵃ f

Proof state:
α : Type u_1
ι : Type u_2
f : α → ι
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ ∏ a : ι, Nat.card (Perm { a_1 // f a_1 = a }) = ∏ i : ι, (Fintype.card { a // f a = i })!

Tactic:
exact Finset.prod_congr rfl fun i _ ↦ by rw [Nat.card_eq_fintype_card, Fintype.card_perm]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma Indep.insert_isCircuit_of_forall_of_nontrivial (hI : M.Indep I) (hInt : I.Nontrivial)
    (he : e ∈ M.closure I) (h : ∀ f ∈ I, e ∉ M.closure (I \ {f})) : M.IsCircuit (insert e I)

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hInt : I.Nontrivial
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
⊢ M.IsCircuit (insert e I)

Tactic:
refine hI.insert_isCircuit_of_forall (fun heI ↦ ?_) he h

Result:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hInt : I.Nontrivial
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
heI : e ∈ I
⊢ False

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hInt : I.Nontrivial
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
heI : e ∈ I
⊢ False

Tactic:
obtain ⟨f, hf, hne⟩ := hInt.exists_ne e

Result:
case intro.intro
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hInt : I.Nontrivial
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
heI : e ∈ I
f : α
hf : f ∈ I
hne : f ≠ e
⊢ False

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hInt : I.Nontrivial
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
heI : e ∈ I
f : α
hf : f ∈ I
hne : f ≠ e
⊢ e ∈ I \ {f}

Tactic:
simp [heI, hne.symm]

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hInt : I.Nontrivial
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
heI : e ∈ I
f : α
hf : f ∈ I
hne : f ≠ e
⊢ False

Tactic:
exact h f hf (mem_closure_of_mem' _ (by simp [heI, hne.symm]))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem cons_xor_cons (x y : BitVec w) (a b : Bool) :
    (cons a x) ^^^ (cons b y) = cons (a ^^ b) (x ^^^ y)

Proof state:
w : Nat
x y : BitVec w
a b : Bool
⊢ cons a x ^^^ cons b y = cons (a ^^ b) (x ^^^ y)

Tactic:
ext i

Result:
case pred
w : Nat
x y : BitVec w
a b : Bool
i : Nat
a✝ : i < w + 1
⊢ (cons a x ^^^ cons b y).getLsbD i = (cons (a ^^ b) (x ^^^ y)).getLsbD i

Proof state:
case pred
w : Nat
x y : BitVec w
a b : Bool
i : Nat
a✝ : i < w + 1
⊢ (cons a x ^^^ cons b y).getLsbD i = (cons (a ^^ b) (x ^^^ y)).getLsbD i

Tactic:
simp [cons]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Impl.lean
theorem mergeTR_go_eq : mergeTR.go le l₁ l₂ acc = acc.reverse ++ merge l₁ l₂ le

Proof state:
case cons
α✝ : Type u_1
le : α✝ → α✝ → Bool
x : α✝
l₁ : List α✝
ih₁ : ∀ {l₂ acc : List α✝}, mergeTR.go le l₁ l₂ acc = acc.reverse ++ l₁.merge l₂ le
l₂ acc : List α✝
⊢ mergeTR.go le (x :: l₁) l₂ acc = acc.reverse ++ (x :: l₁).merge l₂ le

Tactic:
induction l₂ generalizing acc with
| nil => simp [mergeTR.go, merge, reverseAux_eq]
| cons y l₂ ih₂ =>
  simp [mergeTR.go, merge]
  split <;> simp [ih₁, ih₂]

Result:
no goals

Proof state:
case nil
α✝ : Type u_1
le : α✝ → α✝ → Bool
l₂ acc : List α✝
⊢ mergeTR.go le [] l₂ acc = acc.reverse ++ [].merge l₂ le

Tactic:
simp [mergeTR.go, merge, reverseAux_eq]

Result:
no goals

Proof state:
case cons.nil
α✝ : Type u_1
le : α✝ → α✝ → Bool
x : α✝
l₁ : List α✝
ih₁ : ∀ {l₂ acc : List α✝}, mergeTR.go le l₁ l₂ acc = acc.reverse ++ l₁.merge l₂ le
acc : List α✝
⊢ mergeTR.go le (x :: l₁) [] acc = acc.reverse ++ (x :: l₁).merge [] le

Tactic:
simp [mergeTR.go, merge, reverseAux_eq]

Result:
no goals

Proof state:
case cons.cons
α✝ : Type u_1
le : α✝ → α✝ → Bool
x : α✝
l₁ : List α✝
ih₁ : ∀ {l₂ acc : List α✝}, mergeTR.go le l₁ l₂ acc = acc.reverse ++ l₁.merge l₂ le
y : α✝
l₂ : List α✝
ih₂ : ∀ {acc : List α✝}, mergeTR.go le (x :: l₁) l₂ acc = acc.reverse ++ (x :: l₁).merge l₂ le
acc : List α✝
⊢ mergeTR.go le (x :: l₁) (y :: l₂) acc = acc.reverse ++ (x :: l₁).merge (y :: l₂) le

Tactic:
simp [mergeTR.go, merge]

Result:
case cons.cons
α✝ : Type u_1
le : α✝ → α✝ → Bool
x : α✝
l₁ : List α✝
ih₁ : ∀ {l₂ acc : List α✝}, mergeTR.go le l₁ l₂ acc = acc.reverse ++ l₁.merge l₂ le
y : α✝
l₂ : List α✝
ih₂ : ∀ {acc : List α✝}, mergeTR.go le (x :: l₁) l₂ acc = acc.reverse ++ (x :: l₁).merge l₂ le
acc : List α✝
⊢ (if le x y = true then mergeTR.go le l₁ (y :: l₂) (x :: acc) else mergeTR.go le (x :: l₁) l₂ (y :: acc)) =
    acc.reverse ++ if le x y = true then x :: l₁.merge (y :: l₂) le else y :: (x :: l₁).merge l₂ le

Proof state:
α✝ : Type u_1
le : α✝ → α✝ → Bool
l₁ l₂ acc : List α✝
⊢ mergeTR.go le l₁ l₂ acc = acc.reverse ++ l₁.merge l₂ le

Tactic:
induction l₁ generalizing l₂ acc with
| nil => simp [mergeTR.go, merge, reverseAux_eq]
| cons x l₁ ih₁ =>
  induction l₂ generalizing acc with
  | nil => simp [mergeTR.go, merge, reverseAux_eq]
  | cons y l₂ ih₂ =>
    simp [mergeTR.go, merge]
    split <;> simp [ih₁, ih₂]

Result:
no goals

Proof state:
case cons.cons
α✝ : Type u_1
le : α✝ → α✝ → Bool
x : α✝
l₁ : List α✝
ih₁ : ∀ {l₂ acc : List α✝}, mergeTR.go le l₁ l₂ acc = acc.reverse ++ l₁.merge l₂ le
y : α✝
l₂ : List α✝
ih₂ : ∀ {acc : List α✝}, mergeTR.go le (x :: l₁) l₂ acc = acc.reverse ++ (x :: l₁).merge l₂ le
acc : List α✝
⊢ (if le x y = true then mergeTR.go le l₁ (y :: l₂) (x :: acc) else mergeTR.go le (x :: l₁) l₂ (y :: acc)) =
    acc.reverse ++ if le x y = true then x :: l₁.merge (y :: l₂) le else y :: (x :: l₁).merge l₂ le

Tactic:
split <;> simp [ih₁, ih₂]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousWithinAt_prod_of_discrete_right [DiscreteTopology β]
    {f : α × β → γ} {s : Set (α × β)} {x : α × β} :
    ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ⟨·, x.2⟩) {a | (a, x.2) ∈ s} x.1

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s (x.1, x.2) ↔
    ContinuousWithinAt (fun x_1 => f (x_1, (x.1, x.2).2)) {a | (a, (x.1, x.2).2) ∈ s} (x.1, x.2).1

Tactic:
simp_rw [ContinuousWithinAt, nhdsWithin, nhds_prod_eq, nhds_discrete, prod_pure,
← map_inf_principal_preimage]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ Tendsto f (map (fun a => (a, x.2)) (𝓝 x.1 ⊓ 𝓟 ((fun a => (a, x.2)) ⁻¹' s))) (𝓝 (f (x.1, x.2))) ↔
    Tendsto (fun x_1 => f (x_1, x.2)) (𝓝 x.1 ⊓ 𝓟 {a | (a, x.2) ∈ s}) (𝓝 (f (x.1, x.2)))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ Tendsto f (map (fun a => (a, x.2)) (𝓝 x.1 ⊓ 𝓟 ((fun a => (a, x.2)) ⁻¹' s))) (𝓝 (f (x.1, x.2))) ↔
    Tendsto (fun x_1 => f (x_1, x.2)) (𝓝 x.1 ⊓ 𝓟 {a | (a, x.2) ∈ s}) (𝓝 (f (x.1, x.2)))

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (fun x_1 => f (x_1, x.2)) {a | (a, x.2) ∈ s} x.1

Tactic:
rw [← x.eta]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s (x.1, x.2) ↔
    ContinuousWithinAt (fun x_1 => f (x_1, (x.1, x.2).2)) {a | (a, (x.1, x.2).2) ∈ s} (x.1, x.2).1
-- Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
theorem ConcreteCategory.forget_map_eq_coe {X Y : C} (f : X ⟶ Y) : (forget C).map f = f

Proof state:
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X Y : C
f : X ⟶ Y
⊢ (forget C).map f = ⇑(hom f)

Tactic:
with_reducible_and_instances rfl

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X Y : C
f : X ⟶ Y
⊢ (forget C).map f = ⇑(hom f)

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/Ostrowski.lean
lemma padic_le_one (p : ℕ) [Fact p.Prime] (n : ℤ) : padic p n ≤ 1

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
n : ℤ
⊢ (padic p) ↑n ≤ 1

Tactic:
simp only [padic_eq_padicNorm]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
n : ℤ
⊢ ↑(padicNorm p ↑n) ≤ 1

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
n : ℤ
⊢ ↑(padicNorm p ↑n) ≤ 1

Tactic:
exact_mod_cast padicNorm.of_int n

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_intMin (w : Nat) : (intMin w).getLsbD i = decide (i + 1 = w)

Proof state:
i w : Nat
⊢ w - 1 < w ∧ w - 1 = i ↔ i + 1 = w

Tactic:
omega

Result:
no goals

Proof state:
i w : Nat
⊢ (intMin w).getLsbD i = decide (i + 1 = w)

Tactic:
simp only [intMin, getLsbD_twoPow, boolToPropSimps]

Result:
i w : Nat
⊢ w - 1 < w ∧ w - 1 = i ↔ i + 1 = w
-- Mathlib/Analysis/RCLike/Lemmas.lean
theorem reCLM_norm : ‖(reCLM : K →L[ℝ] ℝ)‖ = 1

Proof state:
case h.e'_3
K : Type u_1
inst✝ : RCLike K
⊢ 1 = ‖reCLM 1‖ / ‖1‖

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
⊢ 1 ≤ ‖reLm.mkContinuous 1 ⋯‖

Tactic:
convert ContinuousLinearMap.ratio_le_opNorm (reCLM : K →L[ℝ] ℝ) (1 : K)

Result:
case h.e'_3
K : Type u_1
inst✝ : RCLike K
⊢ 1 = ‖reCLM 1‖ / ‖1‖

Proof state:
K : Type u_1
inst✝ : RCLike K
⊢ ‖reCLM‖ = 1

Tactic:
apply le_antisymm (LinearMap.mkContinuous_norm_le _ zero_le_one _)

Result:
K : Type u_1
inst✝ : RCLike K
⊢ 1 ≤ ‖reLm.mkContinuous 1 ⋯‖
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_mul_I : cos (x * I) = cosh x

Proof state:
x : ℂ
⊢ cosh (x * I * I) = cosh x

Tactic:
ring_nf

Result:
x : ℂ
⊢ cosh (x * I ^ 2) = cosh x

Proof state:
x : ℂ
⊢ cosh (x * I ^ 2) = cosh x

Tactic:
simp

Result:
no goals

Proof state:
x : ℂ
⊢ cos (x * I) = cosh x

Tactic:
rw [← cosh_mul_I]

Result:
x : ℂ
⊢ cosh (x * I * I) = cosh x
-- Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
theorem cardinal_lt_aleph0_of_finiteDimensional [Finite K] [Module.Free K V] [Module.Finite K V] :
    #V < ℵ₀

Proof state:
K : Type u
V : Type v
inst✝⁶ : Ring K
inst✝⁵ : StrongRankCondition K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Finite K
inst✝¹ : Free K V
inst✝ : Module.Finite K V
⊢ #V < ℵ₀

Tactic:
rw [← lift_lt_aleph0.{v, u}, lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank K V]

Result:
K : Type u
V : Type v
inst✝⁶ : Ring K
inst✝⁵ : StrongRankCondition K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Finite K
inst✝¹ : Free K V
inst✝ : Module.Finite K V
⊢ lift.{v, u} #K ^ lift.{u, v} (Module.rank K V) < ℵ₀

Proof state:
K : Type u
V : Type v
inst✝⁶ : Ring K
inst✝⁵ : StrongRankCondition K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Finite K
inst✝¹ : Free K V
inst✝ : Module.Finite K V
⊢ lift.{v, u} #K ^ lift.{u, v} (Module.rank K V) < ℵ₀

Tactic:
exact power_lt_aleph0 (lift_lt_aleph0.2 (lt_aleph0_of_finite K))
  (lift_lt_aleph0.2 (rank_lt_aleph0 K V))

Result:
no goals
-- Mathlib/NumberTheory/Pell.lean
theorem exists_iff_not_isSquare (h₀ : 0 < d) :
    (∃ x y : ℤ, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0) ↔ ¬IsSquare d

Proof state:
case intro.intro.intro.intro
x y : ℤ
hy : y ≠ 0
a : ℤ
h₀ : 0 < a * a
hxy : (x + a * y) * (x - a * y) = 1
⊢ False

Tactic:
simpa [hy, mul_self_pos.mp h₀, sub_eq_add_neg, eq_neg_self_iff] using Int.eq_of_mul_eq_one hxy

Result:
no goals

Proof state:
case intro.intro.intro.intro
x y : ℤ
hy : y ≠ 0
a : ℤ
h₀ : 0 < a * a
hxy : x ^ 2 - a * a * y ^ 2 = 1
⊢ False

Tactic:
rw [← sq, ← mul_pow, sq_sub_sq] at hxy

Result:
case intro.intro.intro.intro
x y : ℤ
hy : y ≠ 0
a : ℤ
h₀ : 0 < a * a
hxy : (x + a * y) * (x - a * y) = 1
⊢ False

Proof state:
d : ℤ
h₀ : 0 < d
⊢ (∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0) → ¬IsSquare d

Tactic:
rintro ⟨x, y, hxy, hy⟩ ⟨a, rfl⟩

Result:
case intro.intro.intro.intro
x y : ℤ
hy : y ≠ 0
a : ℤ
h₀ : 0 < a * a
hxy : x ^ 2 - a * a * y ^ 2 = 1
⊢ False

Proof state:
d : ℤ
h₀ : 0 < d
⊢ (∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0) ↔ ¬IsSquare d

Tactic:
refine ⟨?_, exists_of_not_isSquare h₀⟩

Result:
d : ℤ
h₀ : 0 < d
⊢ (∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0) → ¬IsSquare d
-- Mathlib/Data/Set/Finite/Lattice.lean
lemma map_finite_iSup {F ι : Type*} [CompleteLattice α] [CompleteLattice β] [FunLike F α β]
    [SupBotHomClass F α β] [Finite ι] (f : F) (g : ι → α) :
    f (⨆ i, g i) = ⨆ i, f (g i)

Proof state:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝⁴ : CompleteLattice α
inst✝³ : CompleteLattice β
inst✝² : FunLike F α β
inst✝¹ : SupBotHomClass F α β
inst✝ : Finite ι
f : F
g : ι → α
⊢ f (⨆ i, g i) = ⨆ i, f (g i)

Tactic:
rw [← iSup_univ (f := g), ← iSup_univ (f := fun i ↦ f (g i))]

Result:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝⁴ : CompleteLattice α
inst✝³ : CompleteLattice β
inst✝² : FunLike F α β
inst✝¹ : SupBotHomClass F α β
inst✝ : Finite ι
f : F
g : ι → α
⊢ f (⨆ x ∈ univ, g x) = ⨆ x ∈ univ, f (g x)

Proof state:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝⁴ : CompleteLattice α
inst✝³ : CompleteLattice β
inst✝² : FunLike F α β
inst✝¹ : SupBotHomClass F α β
inst✝ : Finite ι
f : F
g : ι → α
⊢ f (⨆ x ∈ univ, g x) = ⨆ x ∈ univ, f (g x)

Tactic:
exact map_finite_biSup finite_univ f g

Result:
no goals
-- Mathlib/Algebra/BigOperators/GroupWithZero/Finset.lean
lemma prod_ite_zero :
    (∏ i ∈ s, if p i then f i else 0) = if ∀ i ∈ s, p i then ∏ i ∈ s, f i else 0

Proof state:
case neg
ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M₀
s : Finset ι
h : ∃ i ∈ s, ¬p i
⊢ (∏ i ∈ s, if p i then f i else 0) = 0

Tactic:
rcases h with ⟨i, hi, hq⟩

Result:
case neg.intro.intro
ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M₀
s : Finset ι
i : ι
hi : i ∈ s
hq : ¬p i
⊢ (∏ i ∈ s, if p i then f i else 0) = 0

Proof state:
case neg
ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M₀
s : Finset ι
h : ¬∀ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then f i else 0) = 0

Tactic:
push_neg at h

Result:
case neg
ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M₀
s : Finset ι
h : ∃ i ∈ s, ¬p i
⊢ (∏ i ∈ s, if p i then f i else 0) = 0

Proof state:
case pos
ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M₀
s : Finset ι
h : ∀ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then f i else 0) = ∏ i ∈ s, f i

Tactic:
exact prod_congr rfl fun i hi => by simp [h i hi]

Result:
no goals

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M₀
s : Finset ι
i : ι
hi : i ∈ s
hq : ¬p i
⊢ (if p i then f i else 0) = 0

Tactic:
simp [hq]

Result:
no goals

Proof state:
case neg.intro.intro
ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M₀
s : Finset ι
i : ι
hi : i ∈ s
hq : ¬p i
⊢ (∏ i ∈ s, if p i then f i else 0) = 0

Tactic:
exact prod_eq_zero hi (by simp [hq])

Result:
no goals

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M₀
s : Finset ι
⊢ (∏ i ∈ s, if p i then f i else 0) = if ∀ i ∈ s, p i then ∏ i ∈ s, f i else 0

Tactic:
split_ifs with h

Result:
case pos
ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M₀
s : Finset ι
h : ∀ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then f i else 0) = ∏ i ∈ s, f i

case neg
ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M₀
s : Finset ι
h : ¬∀ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then f i else 0) = 0

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M₀
s : Finset ι
h : ∀ i ∈ s, p i
i : ι
hi : i ∈ s
⊢ (if p i then f i else 0) = f i

Tactic:
simp [h i hi]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem ringChar_zmod_n (n : ℕ) : ringChar (ZMod n) = n

Proof state:
n : ℕ
⊢ ringChar (ZMod n) = n

Tactic:
rw [ringChar.eq_iff]

Result:
n : ℕ
⊢ CharP (ZMod n) n

Proof state:
n : ℕ
⊢ CharP (ZMod n) n

Tactic:
exact ZMod.charP n

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem eq_of_degrees_lt_of_eval_index_eq (hvs : Set.InjOn v s) (degree_f_lt : f.degree < #s)
    (degree_g_lt : g.degree < #s) (eval_fg : ∀ i ∈ s, f.eval (v i) = g.eval (v i)) : f = g

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#s)
degree_g_lt : g.degree < ↑(#s)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ (f - g).degree < ↑(#s)

Tactic:
rw [← mem_degreeLT] at degree_f_lt degree_g_lt ⊢

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f ∈ degreeLT R #s
degree_g_lt : g ∈ degreeLT R #s
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ f - g ∈ degreeLT R #s

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#s)
degree_g_lt : g.degree < ↑(#s)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ f = g

Tactic:
refine eq_of_degree_sub_lt_of_eval_index_eq _ hvs ?_ eval_fg

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#s)
degree_g_lt : g.degree < ↑(#s)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ (f - g).degree < ↑(#s)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f ∈ degreeLT R #s
degree_g_lt : g ∈ degreeLT R #s
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ f - g ∈ degreeLT R #s

Tactic:
exact Submodule.sub_mem _ degree_f_lt degree_g_lt

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem snd_comp_quotientMulEquivQuotientProd (I J : Ideal R) (coprime : IsCoprime I J) :
    (RingHom.snd _ _).comp
        (quotientMulEquivQuotientProd I J coprime : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J) =
      Ideal.Quotient.factor mul_le_left

Proof state:
case h
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ ((snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime)).comp (Quotient.mk (I * J)) =
    (factor ⋯).comp (Quotient.mk (I * J))

Tactic:
ext

Result:
case h.a
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
x✝ : R
⊢ (((snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime)).comp (Quotient.mk (I * J))) x✝ =
    ((factor ⋯).comp (Quotient.mk (I * J))) x✝

Proof state:
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ (snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime) = factor ⋯

Tactic:
apply Quotient.ringHom_ext

Result:
case h
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ ((snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime)).comp (Quotient.mk (I * J)) =
    (factor ⋯).comp (Quotient.mk (I * J))

Proof state:
case h.a
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
x✝ : R
⊢ (((snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime)).comp (Quotient.mk (I * J))) x✝ =
    ((factor ⋯).comp (Quotient.mk (I * J))) x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
/-- See `ENNReal.mul_div_cancel_right'` for a stronger version. -/
protected lemma mul_div_cancel_right (hb₀ : b ≠ 0) (hb : b ≠ ∞) : a * b / b = a :=
  ENNReal.mul_div_cancel_right' (by simp [hb₀]) (by simp [hb])

Proof state:
a b : ℝ≥0∞
hb₀ : b ≠ 0
hb : b ≠ ⊤
⊢ b = ⊤ → a = 0

Tactic:
simp [hb]

Result:
no goals

Proof state:
a b : ℝ≥0∞
hb₀ : b ≠ 0
hb : b ≠ ⊤
⊢ b = 0 → a = 0

Tactic:
simp [hb₀]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean
theorem set_walk_length_toFinset_eq (n : ℕ) (u v : V) :
    {p : G.Walk u v | p.length = n}.toFinset = G.finsetWalkLength n u v

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
u v : V
⊢ {p | p.length = n}.toFinset = G.finsetWalkLength n u v

Tactic:
ext p

Result:
case h
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
u v : V
p : G.Walk u v
⊢ p ∈ {p | p.length = n}.toFinset ↔ p ∈ G.finsetWalkLength n u v

Proof state:
case h
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
u v : V
p : G.Walk u v
⊢ p ∈ {p | p.length = n}.toFinset ↔ p ∈ G.finsetWalkLength n u v

Tactic:
simp [← coe_finsetWalkLength_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean
theorem ofReal_arctan (x : ℝ) : (Real.arctan x : ℂ) = arctan x

Proof state:
x : ℝ
⊢ ↑(Real.arctan x) = (↑x).arctan

Tactic:
conv_rhs => rw [← Real.tan_arctan x]

Result:
x : ℝ
⊢ ↑(Real.arctan x) = (↑(Real.tan (Real.arctan x))).arctan

Proof state:
case h₁
x : ℝ
⊢ -(π / 2) < Real.arctan x

Tactic:
exact Real.neg_pi_div_two_lt_arctan _

Result:
no goals

Proof state:
case h₂
x : ℝ
⊢ Real.arctan x ≤ π / 2

Tactic:
exact (Real.arctan_lt_pi_div_two _).le

Result:
no goals

Proof state:
case h₀
x : ℝ
⊢ Real.arctan x ≠ π / 2

Tactic:
exact (Real.arctan_lt_pi_div_two _).ne

Result:
no goals

Proof state:
x : ℝ
⊢ ↑(Real.arctan x) = (↑(Real.tan (Real.arctan x))).arctan

Tactic:
rw [ofReal_tan, arctan_tan]

Result:
case h₀
x : ℝ
⊢ ↑(Real.arctan x) ≠ ↑π / 2

case h₁
x : ℝ
⊢ -(π / 2) < (↑(Real.arctan x)).re

case h₂
x : ℝ
⊢ (↑(Real.arctan x)).re ≤ π / 2

Proof state:
case h₀
x : ℝ
⊢ ¬Real.arctan x = π / 2

Tactic:
rw [← ne_eq]

Result:
case h₀
x : ℝ
⊢ Real.arctan x ≠ π / 2

Proof state:
case h₂
x : ℝ
⊢ (↑(Real.arctan x)).re ≤ π / 2

Tactic:
norm_cast

Result:
case h₂
x : ℝ
⊢ Real.arctan x ≤ π / 2

Proof state:
case h₀
x : ℝ
⊢ ↑(Real.arctan x) ≠ ↑π / 2

case h₁
x : ℝ
⊢ -(π / 2) < (↑(Real.arctan x)).re

case h₂
x : ℝ
⊢ (↑(Real.arctan x)).re ≤ π / 2

Tactic:
all_goals norm_cast

Result:
case h₀
x : ℝ
⊢ ¬Real.arctan x = π / 2

case h₁
x : ℝ
⊢ -(π / 2) < Real.arctan x

case h₂
x : ℝ
⊢ Real.arctan x ≤ π / 2